Theorems · Theorem · measure theory

MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → ℝ),
  MeasureTheory.Integrable f μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), ↑(f x) < g x) ∧
            LowerSemicontinuous g ∧
              MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
                (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Vitali-Carathéodory Theorem: given an integrable real function f, there exists an integrable function g > f which is lower semicontinuous, with integral arbitrarily close to that of f. This function has to be EReal-valued in general.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.WeaklyRegularMeasureTheory.SigmaFinite