English
For a sigma-finite measure μ and an nnreal-valued function f with finite integral, there exists g with g > f everywhere, lower semicontinuous, g finite almost everywhere, and g integrable with its integral strictly less than the integral of f by at least ε > 0.
Русский
При сигма-конечной мере μ и функции f, принимающей значения ℝ≥0 с конечным интегралом, существует g > f повсюду, нижнесемантически непрерывная, конечная почти всюду и интегрируемая, причём ∫ g < ∫ f + ε.
LaTeX
$$$$\\exists g:\\; \\alpha \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\; (∀ x, (f x : \\mathbb{R}_{\\ge 0}^{\\infty}) < g x) \land LowerSemicontinuous(g) \land (∀ᵐ x ∂μ, g x < ∞) \land Integrable (\\lambda x, (g x).toReal) μ \land (\\int x, (g x).toReal ∂μ) < (\\int x, f x ∂μ) + ε.$$$$
Lean4
/-- **Vitali-Carathéodory Theorem**: given an integrable real function `f`, there exists an
integrable function `g > f` which is lower semicontinuous, with integral arbitrarily close
to that of `f`. This function has to be `EReal`-valued in general. -/
theorem exists_lt_lowerSemicontinuous_integral_lt [SigmaFinite μ] (f : α → ℝ) (hf : Integrable f μ) {ε : ℝ}
(εpos : 0 < ε) :
∃ g : α → EReal,
(∀ x, (f x : EReal) < g x) ∧
LowerSemicontinuous g ∧
Integrable (fun x => EReal.toReal (g x)) μ ∧
(∀ᵐ x ∂μ, g x < ⊤) ∧ (∫ x, EReal.toReal (g x) ∂μ) < (∫ x, f x ∂μ) + ε :=
by
let δ : ℝ≥0 := ⟨ε / 2, (half_pos εpos).le⟩
have δpos : 0 < δ := half_pos εpos
let fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)
have int_fp : Integrable (fun x => (fp x : ℝ)) μ := hf.real_toNNReal
rcases exists_lt_lowerSemicontinuous_integral_gt_nnreal fp int_fp δpos with
⟨gp, fp_lt_gp, gpcont, gp_lt_top, gp_integrable, gpint⟩
let fm : α → ℝ≥0 := fun x => Real.toNNReal (-f x)
have int_fm : Integrable (fun x => (fm x : ℝ)) μ := hf.neg.real_toNNReal
rcases exists_upperSemicontinuous_le_integral_le fm int_fm δpos with ⟨gm, gm_le_fm, gmcont, gm_integrable, gmint⟩
let g : α → EReal := fun x => (gp x : EReal) - gm x
have ae_g : ∀ᵐ x ∂μ, (g x).toReal = (gp x : EReal).toReal - (gm x : EReal).toReal :=
by
filter_upwards [gp_lt_top] with _ hx
rw [EReal.toReal_sub] <;> simp [hx.ne]
refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
case int =>
show Integrable (fun x => EReal.toReal (g x)) μ
rw [integrable_congr ae_g]
convert gp_integrable.sub gm_integrable
simp
case intlt =>
show (∫ x : α, (g x).toReal ∂μ) < (∫ x : α, f x ∂μ) + ε
exact
calc
(∫ x : α, (g x).toReal ∂μ) = ∫ x : α, EReal.toReal (gp x) - EReal.toReal (gm x) ∂μ := integral_congr_ae ae_g
_ = (∫ x : α, EReal.toReal (gp x) ∂μ) - ∫ x : α, ↑(gm x) ∂μ :=
by
simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]
exact integral_sub gp_integrable gm_integrable
_ < (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ∫ x : α, ↑(gm x) ∂μ :=
by
apply sub_lt_sub_right
convert gpint
simp only [EReal.toReal_coe_ennreal]
_ ≤ (∫ x : α, ↑(fp x) ∂μ) + ↑δ - ((∫ x : α, ↑(fm x) ∂μ) - δ) := (sub_le_sub_left gmint _)
_ = (∫ x : α, f x ∂μ) + 2 * δ := by simp_rw [integral_eq_integral_pos_part_sub_integral_neg_part hf]; ring
_ = (∫ x : α, f x ∂μ) + ε := by congr 1; simp [field, δ]
case aelt =>
show ∀ᵐ x : α ∂μ, g x < ⊤
filter_upwards [gp_lt_top] with ?_ hx
simp only [g, sub_eq_add_neg, Ne, (EReal.add_lt_top _ _).ne, lt_top_iff_ne_top, lt_top_iff_ne_top.1 hx,
EReal.coe_ennreal_eq_top_iff, not_false_iff, EReal.neg_eq_top_iff, EReal.coe_ennreal_ne_bot]
case lt =>
show ∀ x, (f x : EReal) < g x
intro x
rw [EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (f x)]
refine EReal.sub_lt_sub_of_lt_of_le ?_ ?_ ?_ ?_
· simp only [EReal.coe_ennreal_lt_coe_ennreal_iff]; exact fp_lt_gp x
· simp only [ENNReal.coe_le_coe, EReal.coe_ennreal_le_coe_ennreal_iff]
exact gm_le_fm x
· simp only [EReal.coe_ennreal_ne_bot, Ne, not_false_iff]
· simp only [EReal.coe_nnreal_ne_top, Ne, not_false_iff]
case lsc =>
show LowerSemicontinuous g
apply LowerSemicontinuous.add'
·
exact
continuous_coe_ennreal_ereal.comp_lowerSemicontinuous gpcont fun x y hxy =>
EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
· apply continuous_neg.comp_upperSemicontinuous_antitone _ fun x y hxy => EReal.neg_le_neg_iff.2 hxy
dsimp
apply
continuous_coe_ennreal_ereal.comp_upperSemicontinuous _ fun x y hxy =>
EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
exact ENNReal.continuous_coe.comp_upperSemicontinuous gmcont fun x y hxy => ENNReal.coe_le_coe.2 hxy
· intro x
exact EReal.continuousAt_add (by simp) (by simp)
