Theorems · Theorem · measure theory

ae_eq_const_or_exists_average_ne_compl

∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable f μ →
    f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨
      ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ

If f : α → E is an integrable function, then either it is a.e. equal to the constant ⨍ x, f x ∂μ or there exists a measurable set such that μ t ≠ 0, μ tᶜ ≠ 0, and the average values of f over t and tᶜ are different.

Defined in

Mathlib.Analysis.Convex.Integral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure