tsum_indicator_ne_zero — Mathlib

English

If there exists a ∈ s with f(a) ≠ 0 and f is summable, then the sum over the indicator is nonzero.

Русский

Если существует a в s such that f(a) ≠ 0 и f суммируема, то сумма по s.indicator f не равна нулю.

LaTeX

$$$\\\\mathrm{Summable}(f) \\\\Rightarrow \\\\forall s, \\\\Big( \\\\exists a \\in s, f(a) \\\\neq 0 \\Big) \\\\Rightarrow \\\\sum' x, (s.indicator f) x \\\\neq 0$$$

Lean4

theorem tsum_indicator_ne_zero {f : α → ℝ≥0} (hf : Summable f) {s : Set α} (h : ∃ a ∈ s, f a ≠ 0) :
    (∑' x, (s.indicator f) x) ≠ 0 := fun h' =>
  let ⟨a, ha, hap⟩ := h
  hap ((Set.indicator_apply_eq_self.mpr (absurd ha)).symm.trans ((indicator_summable hf s).tsum_eq_zero_iff.1 h' a))

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