sum of nonneg terms is zero iff terms are zero

Stream: Is there code for X?

[Michael Stoll]

I'm having problems finding the following:

import Mathlib

example {α : Type*} {f : α → ℝ} (hf : Summable f) (hf₀ : ∀ n, 0 ≤ f n) :
    tsum f = 0 ↔ ∀ n, f n = 0 := by sorry

There is docs#tsum_eq_zero_iff, which looks close, but needs a docs#CanonicallyOrderedAddCommMonoid as the target type.

[Michael Stoll]

My attempt:

import Mathlib

lemma tsum_eq_zero_iff_of_summable_of_nonneg {α M : Type*} [OrderedAddCommMonoid M]
    [TopologicalSpace M] [OrderClosedTopology M] {f : α → M} (hf : Summable f)
    (hf₀ : ∀ n, 0 ≤ f n) : tsum f = 0 ↔ ∀ n, f n = 0 := by
  refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
  · contrapose! H
    obtain ⟨n, hn⟩ := H
    replace hn := lt_of_le_of_ne (hf₀ n) hn.symm
    exact (ne_of_lt <| hn.trans_le <| le_tsum hf n fun m _ ↦ hf₀ m).symm
  · convert tsum_zero with n
    exact H n

But it feels like this is missing from Mathlib...

[Terence Tao]

One could convert to an integral and use docs#MeasureTheory.integral_eq_zero_iff_of_nonneg , or convert to ENNReal and use docs#ENNReal.tsum_eq_zero

[Adam Topaz]

Yeah I was going to suggest to use docs#tsum_eq_zero_iff and to convert to NNReal

[Adam Topaz]

I think NNReal should satisfy all the assumptions of that lemma.

[Michael Stoll]

Does this give a nicer proof?

[Patrick Massot]

I can see you are attracted to the golfing side of Mathlib. Don't resist, do it for real:

  · contrapose! H
    exact (H.2.symm.lt_of_le (hf₀ _) |>.trans_le <| le_tsum hf _ fun m _ ↦ hf₀ m).ne'

[Terence Tao]

I'm not such a golf pro but here is my attempt:

import Mathlib

example {α : Type*} {f : α → ℝ} (hf : Summable f) (hf₀ : ∀ n, 0 ≤ f n) : tsum f = 0 ↔ ∀ n, f n = 0 := by
  constructor
  . intro hsum
    have := (ENNReal.ofReal_tsum_of_nonneg hf₀ hf).symm
    rw [hsum] at this; simp at this
    intro n; linarith [this n, hf₀ n]
  intro h0
  rw [tsum_congr h0]
  simp

[Michael Stoll]

But my version is more general :smile:

[Michael Stoll]

Slightly more golfed:

lemma tsum_eq_zero_iff_of_summable_of_nonneg {α M : Type*} [OrderedAddCommMonoid M]
    [TopologicalSpace M] [OrderClosedTopology M] {f : α → M} (hf : Summable f)
    (hf₀ : ∀ n, 0 ≤ f n) : tsum f = 0 ↔ ∀ n, f n = 0 := by
  refine ⟨fun H ↦ ?_, fun H ↦ by convert tsum_zero; exact H _⟩
  contrapose! H
  obtain ⟨n, hn⟩ := H
  exact (lt_of_le_of_ne (hf₀ n) hn.symm |>.trans_le <| le_tsum hf n fun m _ ↦ hf₀ m).ne'