English
For any set s and function f, the lintegral of s.indicator f is bounded above by the lintegral of f over s.
Русский
Для множества s и функции f линегральный интеграл индикатора s.indicator f не превышает линеграл интеграла f на s.
LaTeX
$$$$ \\int^- a, s.indicator f(a) \\, d\\mu \\le \\int^- a \\in s, f(a) \\, d\\mu. $$$$
Lean4
theorem lintegral_indicator_le (f : α → ℝ≥0∞) (s : Set α) : ∫⁻ a, s.indicator f a ∂μ ≤ ∫⁻ a in s, f a ∂μ :=
by
simp only [lintegral]
apply iSup_le (fun g ↦ (iSup_le (fun hg ↦ ?_)))
have : g ≤ f := hg.trans (indicator_le_self s f)
refine le_iSup_of_le g (le_iSup_of_le this (le_of_eq ?_))
rw [lintegral_restrict, SimpleFunc.lintegral]
congr with t
by_cases H : t = 0
· simp [H]
congr with x
simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and]
rintro rfl
contrapose! H
simpa [H] using hg x
