Theorems · Theorem · measure theory

MeasureTheory.exists_upperSemicontinuous_le_integral_le

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] (f : α → NNReal),
  MeasureTheory.Integrable (fun x => ↑(f x)) μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), g x ≤ f x) ∧
            UpperSemicontinuous g ∧
              MeasureTheory.Integrable (fun x => ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ε ≤ ∫ (x : α), ↑(g x) ∂μ

Given an integrable function f with values in ℝ≥0, there exists an upper semicontinuous function g ≤ f with integral arbitrarily close to that of f. Formulation in terms of integral. 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 254 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.WeaklyRegular