English
For an integrable real-valued function f on a sigma-finite measure space, there exists an integrable upper bound g with g > f almost everywhere, lower semicontinuous, and the integral of g is arbitrarily close to the integral of f from below in the extended sense.
Русский
Для интегрируемой вещественно-значной функции f на сигма-конечной мере существует интегрируемое верхнее ограничение g, удовлетворяющее g > f почти везде, являющееся нижне полунепрерывной и с интегралом ближе к интегралу f снизу.
LaTeX
$$$$\\exists g:\\; \\alpha \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\quad (\\forall x, g(x) \\le f(x)) \land UpperSemicontinuous(g) \land (\\int^{-} x, f(x) \\partial \\mu) \\le (\\int^{-} x, g(x) \\partial \\mu) + \\varepsilon.$$$$
Lean4
/-- 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
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. -/
theorem exists_upperSemicontinuous_le_lintegral_le (f : α → ℝ≥0) (int_f : (∫⁻ x, f x ∂μ) ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
∃ g : α → ℝ≥0, (∀ x, g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε :=
by
obtain ⟨fs, fs_le_f, int_fs⟩ : ∃ fs : α →ₛ ℝ≥0, (∀ x, fs x ≤ f x) ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 :=
by
have := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => by simp⟩]
simp only [lt_iSup_iff] at this
rcases this with ⟨fs, fs_le_f, int_fs⟩
refine ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, ?_⟩
convert int_fs.le
rw [← SimpleFunc.lintegral_eq_lintegral]
simp only [SimpleFunc.coe_map, Function.comp_apply]
have int_fs_lt_top : (∫⁻ x, fs x ∂μ) ≠ ∞ :=
by
refine ne_top_of_le_ne_top int_f (lintegral_mono fun x => ?_)
simpa only [ENNReal.coe_le_coe] using fs_le_f x
obtain ⟨g, g_le_fs, gcont, gint⟩ :
∃ g : α → ℝ≥0, (∀ x, g x ≤ fs x) ∧ UpperSemicontinuous g ∧ (∫⁻ x, fs x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε / 2 :=
fs.exists_upperSemicontinuous_le_lintegral_le int_fs_lt_top (ENNReal.half_pos ε0).ne'
refine ⟨g, fun x => (g_le_fs x).trans (fs_le_f x), gcont, ?_⟩
calc
(∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := int_fs
_ ≤ (∫⁻ x, g x ∂μ) + ε / 2 + ε / 2 := (add_le_add gint le_rfl)
_ = (∫⁻ x, g x ∂μ) + ε := by rw [add_assoc, ENNReal.add_halves]
