indicator_summable — Mathlib

English

If f is summable and s is a set, then s.indicator f is summable.

Русский

Если f суммируема, то и indicator по подмножеству s также суммируема.

LaTeX

$$$\\\\mathrm{Summable}(f) \\\\Rightarrow \\\\mathrm{Summable}(s\\\\text{.indicator } f)$$$

Lean4

theorem indicator_summable {f : α → ℝ≥0} (hf : Summable f) (s : Set α) : Summable (s.indicator f) := by
  classical
  refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe

Похожие утверждения