English
Let f be a nonnegative function; there exists g ≤ f, lower than f, which is upper semicontinuous and whose lintegral is within ε of that of f from above.
Русский
Пусть f неотрицательна; существует g ≤ f, с g выше f, являющееся верхнеполупрерывной, и лин-интеграл g ближе к интегралу f на ε сверху.
LaTeX
$$$$\\exists g:\\; \\alpha \\to \\mathbb{R}_{\\ge 0},\\quad (∀ x, g(x) \\le f(x)) ∧ UpperSemicontinuous(g) ∧ (\\int^{-} x, f(x) ∂μ) ≤ (\\int^{-} x, g(x) ∂μ) + ε.$$$$
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
`integral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. -/
theorem exists_upperSemicontinuous_le_integral_le (f : α → ℝ≥0) (fint : Integrable (fun x => (f x : ℝ)) μ) {ε : ℝ}
(εpos : 0 < ε) :
∃ g : α → ℝ≥0,
(∀ x, g x ≤ f x) ∧
UpperSemicontinuous g ∧ Integrable (fun x => (g x : ℝ)) μ ∧ (∫ x, (f x : ℝ) ∂μ) - ε ≤ ∫ x, ↑(g x) ∂μ :=
by
lift ε to ℝ≥0 using εpos.le
rw [NNReal.coe_pos, ← ENNReal.coe_pos] at εpos
have If : (∫⁻ x, f x ∂μ) < ∞ := hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral
rcases exists_upperSemicontinuous_le_lintegral_le f If.ne εpos.ne' with ⟨g, gf, gcont, gint⟩
have Ig : (∫⁻ x, g x ∂μ) < ∞ := by
refine lt_of_le_of_lt (lintegral_mono fun x => ?_) If
simpa using gf x
refine ⟨g, gf, gcont, ?_, ?_⟩
· refine Integrable.mono fint gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall fun x => by simp [gf x]
· rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
· rw [sub_le_iff_le_add]
convert ENNReal.toReal_mono _ gint
· simp
· rw [ENNReal.toReal_add Ig.ne ENNReal.coe_ne_top]; simp
· simpa using Ig.ne
· apply Filter.Eventually.of_forall; simp
· exact gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable
· apply Filter.Eventually.of_forall; simp
· exact fint.aestronglyMeasurable
