English
If a sequence g ≤ f has finite sum ∑' i g(i) ≠ ∞, then the sum of the pointwise differences equals the difference of sums: ∑' i (f(i) − g(i)) = (∑' i f(i)) − (∑' i g(i)).
Русский
Пусть g(i) ≤ f(i) и ∑' i g(i) ≠ ∞. Тогда сумма по точечных разностям равна разности сумм: ∑' i (f(i) − g(i)) = (∑' i f(i)) − (∑' i g(i)).
LaTeX
$$$\left(\sum\' i\, g(i) \neq \infty\right) \wedge (g \le f) \;\Rightarrow\; \sum\' i \ (f(i)-g(i)) = \sum\' i \ f(i) - \sum\' i \ g(i).$$$
Lean4
/-- The sum over the complement of a finset tends to `0` when the finset grows to cover the whole
space. This does not need a summability assumption, as otherwise all sums are zero. -/
theorem tendsto_tsum_compl_atTop_zero {α : Type*} {f : α → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) :
Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0) :=
by
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
convert ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)
rw [ENNReal.coe_tsum]
exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective
