exists_lt_lowerSemicontinuous_lintegral_ge

English

Let μ be a sigma-finite measure on a space α and f a measurable function taking values in ℝ≥0. For every ε > 0 there exists a lower semicontinuous function g: α → ℝ≥0∞ with g(x) > f(x) for all x and whose integral is within ε of the integral of f, i.e., ∫ g ≤ ∫ f + ε.

Русский

Пусть μ — сигма-мера над пространством α, а f — измеримая функция, принимающая значения в ℝ≥0. Для любого ε > 0 существует функция g, которая ниже f точечно и является нижне полунепрерывной на α, причём ∫ g ≤ ∫ f + ε.

LaTeX

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

Lean4

/-- 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`. -/
theorem exists_lt_lowerSemicontinuous_lintegral_ge [SigmaFinite μ] (f : α → ℝ≥0) (fmeas : Measurable 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_pos_lintegral_lt_of_sigmaFinite μ this with ⟨w, wpos, wmeas, wint⟩
  let f' x := ((f x + w x : ℝ≥0) : ℝ≥0∞)
  rcases exists_le_lowerSemicontinuous_lintegral_ge μ f' (fmeas.add wmeas).coe_nnreal_ennreal this with
    ⟨g, le_g, gcont, gint⟩
  refine ⟨g, fun x => ?_, gcont, ?_⟩
  ·
    calc
      (f x : ℝ≥0∞) < f' x := by simpa only [← ENNReal.coe_lt_coe, add_zero] using add_lt_add_left (wpos x) (f x)
      _ ≤ g x := le_g x
  ·
    calc
      (∫⁻ x : α, g x ∂μ) ≤ (∫⁻ x : α, f x + w x ∂μ) + ε / 2 := gint
      _ = ((∫⁻ x : α, f x ∂μ) + ∫⁻ x : α, w x ∂μ) + ε / 2 := by rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε / 2 + ε / 2 := by grw [wint]
      _ = (∫⁻ x : α, f x ∂μ) + ε := by rw [add_assoc, ENNReal.add_halves]

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