English
If ∫ f dμ < ∞, there exists a measurable g ≤ f with the same integrals on all measurable sets.
Русский
Если ∫ f dμ < ∞, существует измеримая g ≤ f такая, что интегралы по всем измеримым множествам совпадают.
LaTeX
$$$\\exists g, Measurable\\ g \\land g ≤ f \\land ∀ s, MeasurableSet s → ∫⁻ a in s, f a ∂μ = ∫⁻ a in s, g a ∂μ$$$
Lean4
/-- For any function `f : α → ℝ≥0∞`, there exists a measurable function `g ≤ f` with the same
integral over any measurable set. -/
theorem exists_measurable_le_setLIntegral_eq_of_integrable {f : α → ℝ≥0∞} (hf : ∫⁻ a, f a ∂μ ≠ ∞) :
∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ s : Set α, MeasurableSet s → ∫⁻ a in s, f a ∂μ = ∫⁻ a in s, g a ∂μ :=
by
obtain ⟨g, hmg, hgf, hifg⟩ := exists_measurable_le_lintegral_eq (μ := μ) f
use g, hmg, hgf
refine fun s hms ↦ le_antisymm ?_ (lintegral_mono hgf)
rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]
· gcongr; apply hgf
· rw [hifg] at hf
exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)
· exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)
