tsum_eapproxDiff — Mathlib

English

For f: α→ℝ≥0∞, the sum over k=0..n of eapproxDiff f k a equals eapprox f n a.

Русский

Сумма по k=0..n eapproxDiff f k a равна eapprox f n a.

LaTeX

$$$ \sum_{k=0}^{n} (eapproxDiff\ f\ k\ a) = eapprox\ f\ n\ a $$$

Lean4

theorem tsum_eapproxDiff (f : α → ℝ≥0∞) (hf : Measurable f) (a : α) : (∑' n, (eapproxDiff f n a : ℝ≥0∞)) = f a := by
  simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff, iSup_eapprox_apply hf a]

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