Theorems · Theorem · measure theory

StrictConvex.ae_eq_const_or_average_mem_interior

∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsFiniteMeasure μ],
  StrictConvex ℝ s →
    IsClosed s →
      (∀ᵐ (x : α) ∂μ, f x ∈ s) →
        MeasureTheory.Integrable f μ → f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s

If an integrable function f : α → E takes values in a strictly convex closed set s, then either it is a.e. equal to its average value, or its average value belongs to the interior of s.

Defined in

Mathlib.Analysis.Convex.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure