English
For f : α → ℝ with f integrable, there exists g : α → EReal, with g < f everywhere, g upper semicontinuous, g integrable, and ∫ g > ∫ f − ε.
Русский
Для интегрируемой f : α → ℝ существует g : α → EReal, такой что g(x) < f(x) для всех x, g верхнеполупрерывна, интегрируема, и ∫ g > ∫ f − ε.
LaTeX
$$$$\\exists g:\\; \\alpha \\to \\mathrm{EReal},\\quad (\\forall x, g(x) < f(x)) \land UpperSemicontinuous(g) \land Integrable (\\lambda x, EReal.toReal(g x)) μ \land (\\forall^{*} x ∂μ, 0 < g x) \land (\\int x, f x ∂μ) < (\\int x, EReal.toReal(g x) ∂μ) + ε.$$$$
Lean4
/-- **Vitali-Carathéodory Theorem**: given an integrable real function `f`, there exists an
integrable function `g < f` which is upper semicontinuous, with integral arbitrarily close to that
of `f`. This function has to be `EReal`-valued in general. -/
theorem exists_upperSemicontinuous_lt_integral_gt [SigmaFinite μ] (f : α → ℝ) (hf : Integrable f μ) {ε : ℝ}
(εpos : 0 < ε) :
∃ g : α → EReal,
(∀ x, (g x : EReal) < f x) ∧
UpperSemicontinuous g ∧
Integrable (fun x => EReal.toReal (g x)) μ ∧
(∀ᵐ x ∂μ, ⊥ < g x) ∧ (∫ x, f x ∂μ) < (∫ x, EReal.toReal (g x) ∂μ) + ε :=
by
rcases exists_lt_lowerSemicontinuous_integral_lt (fun x => -f x) hf.neg εpos with
⟨g, g_lt_f, gcont, g_integrable, g_lt_top, gint⟩
refine ⟨fun x => -g x, ?_, ?_, ?_, ?_, ?_⟩
· exact fun x => EReal.neg_lt_comm.1 (by simpa only [EReal.coe_neg] using g_lt_f x)
· exact continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy => EReal.neg_le_neg_iff.2 hxy
· convert g_integrable.neg
simp
· simpa [bot_lt_iff_ne_bot, lt_top_iff_ne_top] using g_lt_top
· simp_rw [integral_neg, lt_neg_add_iff_add_lt] at gint
rw [add_comm] at gint
simpa [integral_neg] using gint
