exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable

English

Let μ be sigma-finite and f : α → ℝ≥0 be almost everywhere measurable with values in ℝ≥0. For every ε > 0 there exists a lower semicontinuous g: α → ℝ≥0∞ such that g > f everywhere, and the integral of g is within ε of the integral of f.

Русский

Пусть μ — сигма-плотная мера и f : α → ℝ≥0 почти всюду измерима. Для любого ε > 0 существует нижнесомножно непрерывная функция g: α → ℝ≥0∞ такая, что g(x) > f(x) для всех x и интеграл g близок к интегралу f на ε.

LaTeX

$$$$\\exists g:\\; \\alpha \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\quad (\\forall x, (f(x) : \\mathbb{R}_{\\ge 0}^{\\infty}) < g(x)) \\,\\land \\, LowerSemicontinuous(g) \\,\\land \\, (\\int^{-} x, g(x) \\partial \\mu) \\le (\\int^{-} x, f(x) \\partial \\mu) + \\varepsilon.$$$$

Lean4

/-- Given an almost everywhere 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`. -/
theorem exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable [SigmaFinite μ] (f : α → ℝ≥0)
    (fmeas : AEMeasurable f μ) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0∞, (∀ x, (f x : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε :=
  by
  have : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'
  rcases exists_lt_lowerSemicontinuous_lintegral_ge μ (fmeas.mk f) fmeas.measurable_mk this with
    ⟨g0, f_lt_g0, g0_cont, g0_int⟩
  rcases exists_measurable_superset_of_null fmeas.ae_eq_mk with ⟨s, hs, smeas, μs⟩
  rcases
    exists_le_lowerSemicontinuous_lintegral_ge μ (s.indicator fun _x => ∞) (measurable_const.indicator smeas) this with
    ⟨g1, le_g1, g1_cont, g1_int⟩
  refine ⟨fun x => g0 x + g1 x, fun x => ?_, g0_cont.add g1_cont, ?_⟩
  · by_cases h : x ∈ s
    · have := le_g1 x
      simp only [h, Set.indicator_of_mem, top_le_iff] at this
      simp [this]
    · have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h
      rw [this]
      exact (f_lt_g0 x).trans_le le_self_add
  ·
    calc
      ∫⁻ x, g0 x + g1 x ∂μ = (∫⁻ x, g0 x ∂μ) + ∫⁻ x, g1 x ∂μ := lintegral_add_left g0_cont.measurable _
      _ ≤ (∫⁻ x, f x ∂μ) + ε / 2 + (0 + ε / 2) := by
        refine add_le_add ?_ ?_
        · convert g0_int using 2
          exact lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)
        · convert g1_int
          simp only [smeas, μs, lintegral_const, Set.univ_inter, MeasurableSet.univ, lintegral_indicator, mul_zero,
            restrict_apply]
      _ = (∫⁻ x, f x ∂μ) + ε := by simp only [add_assoc, ENNReal.add_halves, zero_add]

Похожие утверждения