tsum_eq_add_tsum_ite — Mathlib

English

For summable f, the total sum equals f(i) plus the sum over the rest with an indicator that excludes i.

Русский

Для суммируемой f сумма равна f(i) плюс сумма по остальным с индикатором исключения i.

LaTeX

$$$\\\\mathrm{Summable}(f) \\\\Rightarrow \\\\forall i, \\\\sum' x, f x = f i + \\\\sum' x, \\mathrm{ite}(x=i) 0 (f x)$$$

Lean4

theorem tsum_eq_add_tsum_ite {f : α → ℝ≥0} (hf : Summable f) (i : α) : ∑' x, f x = f i + ∑' x, ite (x = i) 0 (f x) :=
  by
  refine (NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i
  rw [Function.update_apply]
  split_ifs <;> simp only [zero_le', le_rfl]

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