English
For any function f, there exists a measurable g such that g ≤ f almost everywhere and ∫ f = ∫ g.
Русский
Для любой функции существует измеримая g ≤ f почти везде и равный интеграл: ∫ f = ∫ g.
LaTeX
$$$$ \exists g: \alpha \to \mathbb{R}_{\ge 0}^∞,\ Measurable(g) \wedge (∀ a, g(a) \le f(a)) \wedge \int^- a, f(a) \partial \mu = \int^- a, g(a) \partial \mu. $$$$
Lean4
/-- For any function `f : α → ℝ≥0∞`, there exists a measurable function `g ≤ f` with the same
integral. -/
theorem exists_measurable_le_lintegral_eq (f : α → ℝ≥0∞) :
∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∫⁻ a, f a ∂μ = ∫⁻ a, g a ∂μ :=
by
rcases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ | h₀
· exact ⟨0, measurable_zero, zero_le f, h₀.trans lintegral_zero.symm⟩
rcases exists_seq_strictMono_tendsto' h₀.bot_lt with ⟨L, _, hLf, hL_tendsto⟩
have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ a, g a ∂μ :=
by
intro n
simpa only [← iSup_lintegral_measurable_le_eq_lintegral f, lt_iSup_iff, exists_prop] using (hLf n).2
choose g hgm hgf hLg using this
refine ⟨fun x => ⨆ n, g n x, .iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm ?_ ?_⟩
· refine le_of_tendsto' hL_tendsto fun n => (hLg n).le.trans <| lintegral_mono fun x => ?_
exact le_iSup (fun n => g n x) n
· exact lintegral_mono fun x => iSup_le fun n => hgf n x
