Infinite sum is zero iff every term is zero

Stream: new members

[João Camarneiro]

Hello! In trying to prove something, I found myself wanting to use the following result.

example (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≥ 0) (h' : Summable g) :
       ∑' (i : ℕ), g i = 0 ↔ ∀ (i : ℕ), g i = 0 := sorry

Is this in mathlib or is there an easy way to establish this? I know that, if the return type of g were NNReal instead, this is simply docs#tsum_eq_zero_iff. However, it seems like a hassle to have to change everything concerning g because of this, and I believe the result would also be useful in this form.

[Anatole Dedecker]

We have docs#hasSum_zero_iff_of_nonneg, but weirdly enough we don’t seem to have the tsum version

[João Camarneiro]

Anatole Dedecker said:

We have docs#hasSum_zero_iff_of_nonneg, but weirdly enough we don’t seem to have the tsum version

Thank you! With that, this does the trick:

example (g : ℕ → ℝ) (h : ∀ (i : ℕ), g i ≥ 0) (h' : Summable g) :
    ∑' (i : ℕ), g i = 0 ↔ ∀ (i : ℕ), g i = 0 := by
  calc
    _ ↔ HasSum g 0 := (Summable.hasSum_iff h').symm
    _ ↔ g = 0 := hasSum_zero_iff_of_nonneg h
    _ ↔ _ := Function.funext_iff