tsum_sub — Mathlib

English

If (a_i) and (b_i) are nonnegative with a_i ≥ b_i, and ∑' i b_i converges, then ∑' i (a_i − b_i) = ∑' i a_i − ∑' i b_i.

Русский

Пусть a_i ≥ b_i, сумма ∑' i b_i сходится; тогда ∑' i (a_i − b_i) = ∑' i a_i − ∑' i b_i.

LaTeX

$$$\left(\sum' i, b_i \neq \infty\right) \wedge (b_i \le a_i) \Rightarrow \sum' i (a_i - b_i) = \sum' i a_i - \sum' i b_i.$$$

Lean4

theorem tsum_sub {f : ℕ → ℝ≥0∞} {g : ℕ → ℝ≥0∞} (h₁ : ∑' i, g i ≠ ∞) (h₂ : g ≤ f) :
    ∑' i, (f i - g i) = ∑' i, f i - ∑' i, g i :=
  have : ∀ i, f i - g i + g i = f i := fun i => tsub_add_cancel_of_le (h₂ i)
  ENNReal.eq_sub_of_add_eq h₁ <| by simp only [← ENNReal.tsum_add, this]

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