tsum_eq_add_tsum_ite — Mathlib

English

A generalization of splitting a sum by an indicator: sum over all equals the distinguished term plus the sum over the rest with an if-then-else guard.

Русский

Обобщение разложения суммы по индикатору: сумма по всему равна члену с помеченным индексом плюс сумма по остаткам с защитой по условию.

LaTeX

$$$\sum' x, f x = f b + \sum' x, \mathrm{ite}(x = b, 0, f x).$$$

Lean4

theorem tsum_eq_add_tsum_ite {f : β → ℝ≥0∞} (b : β) : ∑' x, f x = f b + ∑' x, ite (x = b) 0 (f x) :=
  ENNReal.summable.tsum_eq_add_tsum_ite' b

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