Theorems · Theorem · measure theory

MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → NNReal),
  Measurable f →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

Given a measurable function f with values in ℝ≥0 in a sigma-finite space, there exists a lower semicontinuous function g > f with integral arbitrarily close to that of f. Formulation in terms of lintegral. Auxiliary lemma for Vitali-Carathéodory theorem exists_lt_lower_semicontinuous_integral_lt.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.WeaklyRegularMeasureTheory.SigmaFinite