English
If f ≤ g almost everywhere, then the lintegral of f is ≤ the lintegral of g.
Русский
Если f ≤ g почти повсюду, то линеграл f ≤ линеграл g.
LaTeX
$$$$ \forall f,g: \alpha \to \mathbb{R}_{\ge 0}^∞,\ (f \le^a.e. g) \Rightarrow \int^- a, f(a) \partial \mu \le \int^- a, g(a) \partial \mu. $$$$
Lean4
theorem lintegral_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=
by
rcases exists_measurable_superset_of_null h with ⟨t, hts, ht, ht0⟩
have : ∀ᵐ x ∂μ, x ∉ t := measure_eq_zero_iff_ae_notMem.1 ht0
rw [lintegral, lintegral]
refine iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_
· intro a
by_cases h : a ∈ t <;>
simp only [restrict_apply s ht.compl, mem_compl_iff, h, not_true, not_false_eq_true, indicator_of_notMem, zero_le,
not_false_eq_true, indicator_of_mem]
exact le_trans (hfs a) (by_contradiction fun hnfg => h (hts hnfg))
· refine le_of_eq (SimpleFunc.lintegral_congr <| this.mono fun a hnt => ?_)
by_cases hat : a ∈ t <;>
simp only [restrict_apply s ht.compl, mem_compl_iff, hat, not_true, not_false_eq_true, indicator_of_notMem,
not_false_eq_true, indicator_of_mem]
exact (hnt hat).elim
