English
There exists a measurable g with g ≤ f and the same lintegral as f.
Русский
Существует измеримая g ≤ f с тем же линегралом что и f.
LaTeX
$$$$ ∃ g: α \to \mathbb{R}_{\ge 0}^∞,\ Measurable(g) ∧ (∀ a, g(a) ≤ f(a)) ∧ ∫^- a, f(a) ∂μ = ∫^- a, g(a) ∂μ. $$$$
Lean4
/-- Lebesgue integral over a set is monotone in function.
This version assumes that the upper estimate is an a.e. measurable function
and the estimate holds a.e. on the set.
See also `setLIntegral_mono_ae'` for a version that assumes measurability of the set
but assumes no regularity of either function. -/
theorem setLIntegral_mono_ae {s : Set α} {f g : α → ℝ≥0∞} (hg : AEMeasurable g (μ.restrict s))
(hfg : ∀ᵐ x ∂μ, x ∈ s → f x ≤ g x) : ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in s, g x ∂μ :=
by
rcases exists_measurable_le_lintegral_eq (μ.restrict s) f with ⟨f', hf'm, hle, hf'⟩
rw [hf']
apply lintegral_mono_ae
rw [ae_restrict_iff₀]
· exact hfg.mono fun x hx hxs ↦ (hle x).trans (hx hxs)
· exact nullMeasurableSet_le hf'm.aemeasurable hg
