Reference · Finite sums

rainbow.math.sums.nonneg-zero

Finite sumssrc/rainbow/math/sums/nonneg_zero.clj0 definitions, 3 theorems

Nonnegative terms that sum to zero are each zero, over signed/expr-sum-value: if 0 <= F i for every i < k and sum F k ~ 0 then F i ~ 0 for every i < k. The two-term step: 0 <= a, 0 <= b, a + b ~ 0 give a ~ 0 (a <= a + b ~ 0 and 0 <= a) and then b ~ 0. The induction peels the last term.

signed/nonnegative-pair-sum-zero :
  (a b : ℚ)
  (ha : 0 ≤ a)
  (hb : 0 ≤ b)
  (hab : a + b = 0)
  → proposition/conjunction (a = 0) (b = 0)

signed/expr-sum-value-nonnegative :
  (F : ℕ → ℚ) (k : ℕ)
  (hF : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx k), 0 ≤ F idx)
  → 0 ≤ signed/expr-sum-value F k

signed/expr-sum-value-nonnegative-terms-zero :
  (F : ℕ → ℚ) (k : ℕ)
  (hF : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx k), 0 ≤ F idx)
  (hs : signed/expr-sum-value F k = 0)
  (idx : ℕ) (bound : nat/strict-below idx k)
  → F idx = 0