English
Let μ be sigma-finite and f: α → ℝ≥0 with finite real integral. Then there exists g: α → ℝ≥0∞ such that g > f pointwise, g is lower semicontinuous, g is integrable in the extended real sense, and its integral is strictly less than the integral of f plus a given ε > 0.
Русский
Пусть μ — сигма-мера, f: α → ℝ≥0 имеет конечный интеграл. Тогда существует g: α → ℝ≥0∞ such that g(x) > f(x) для всех x, g → нижняя полуприводимая, и интеграл g меньше интеграла f плюс заданное ε > 0.
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 \\, (\\forall^{*} x, g(x) < \\top) \\,\\land \\, Integrable (\\lambda x, (g(x))^{\\toReal}) \\, \\mu \\, \\land \\, (\\int^{-} x, g(x) \\partial \\mu) < (\\int^{-} x, f(x) \\partial \\mu) + \\varepsilon.$$$$
Lean4
/-- Given an integrable 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 `integral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. -/
theorem exists_lt_lowerSemicontinuous_integral_gt_nnreal [SigmaFinite μ] (f : α → ℝ≥0)
(fint : Integrable (fun x => (f x : ℝ)) μ) {ε : ℝ} (εpos : 0 < ε) :
∃ g : α → ℝ≥0∞,
(∀ x, (f x : ℝ≥0∞) < g x) ∧
LowerSemicontinuous g ∧
(∀ᵐ x ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ (∫ x, (g x).toReal ∂μ) < (∫ x, ↑(f x) ∂μ) + ε :=
by
have fmeas : AEMeasurable f μ :=
by
convert fint.aestronglyMeasurable.real_toNNReal.aemeasurable
simp only [Real.toNNReal_coe]
lift ε to ℝ≥0 using εpos.le
obtain ⟨δ, δpos, hδε⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ δ < ε := exists_between εpos
have int_f_ne_top : (∫⁻ a : α, f a ∂μ) ≠ ∞ := (hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral).ne
rcases exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable μ f fmeas (ENNReal.coe_ne_zero.2 δpos.ne') with
⟨g, f_lt_g, gcont, gint⟩
have gint_ne : (∫⁻ x : α, g x ∂μ) ≠ ∞ := ne_top_of_le_ne_top (by simpa) gint
have g_lt_top : ∀ᵐ x : α ∂μ, g x < ∞ := ae_lt_top gcont.measurable gint_ne
have Ig : (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) = ∫⁻ a : α, g a ∂μ :=
by
apply lintegral_congr_ae
filter_upwards [g_lt_top] with _ hx
simp only [hx.ne, ENNReal.ofReal_toReal, Ne, not_false_iff]
refine ⟨g, f_lt_g, gcont, g_lt_top, ?_, ?_⟩
· refine ⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩
simp only [hasFiniteIntegral_iff_norm, Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
convert gint_ne.lt_top using 1
· rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
·
calc
ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) = ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
_ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) :=
by
apply ENNReal.toReal_mono _ gint
simpa using int_f_ne_top
_ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
_ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := (add_lt_add_left hδε _)
_ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
· apply Filter.Eventually.of_forall fun x => _; simp
· exact fmeas.coe_nnreal_real.aestronglyMeasurable
· apply Filter.Eventually.of_forall fun x => _; simp
· apply gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable
