Reference · Finite sums

rainbow.math.sums.two-terms

Finite sumssrc/rainbow/math/sums/two_terms.clj0 definitions, 2 theorems

One term, and two DISTINCT terms, are bounded by a nonnegative expr-sum-value. Reuses the existing sum and order. F is intentionally not named q: s/induct binds q.

Depends onmath.sums.nonneg-zero

signed/expr-sum-value-term-bound :
  (F : ℕ → ℚ) (n : ℕ)
  (hF : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ F idx)
  (i : ℕ) (hi : nat/strict-below i n)
  → F i ≤ signed/expr-sum-value F n

signed/expr-sum-value-two-distinct-bound :
  (F : ℕ → ℚ) (n : ℕ)
  (hF : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ F idx)
  (i : ℕ) (hi : nat/strict-below i n) (j : ℕ) (hj : nat/strict-below j n)
  (hne : proposition/negation (i = j))
  → F i + F j ≤ signed/expr-sum-value F n