Theorems · Theorem · measure theory

MeasureTheory.integral_def

∀ {α : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → G),
  MeasureTheory.integral μ f =
    if x_1 : CompleteSpace G then
      if hf : MeasureTheory.Integrable f μ then MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf) else 0
    else 0

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

41 results in Mathlib

Foundations

Depth 250 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace