Reference · Finite sums

rainbow.math.sums.single-support

Finite sumssrc/rainbow/math/sums/single_support.clj0 definitions, 6 theorems

Single supported terms and tight finite unit-capacity sums.

Depends onmath.sums.one-hot-indexmath.sums.of-natmath.sums.nonblocking

nat/below-implies-distinct :
  (i j : ℕ) (below : nat/strict-below i j)
  → proposition/negation (i = j)

signed/expr-sum-single-support :
  (F : ℕ → ℚ) (i n : ℕ) (bound : nat/strict-below i n)
  (support : ∀ (index18513 : ℕ), ∀ (bound18514 : nat/strict-below index18513 n), ∀ (distinct18515 : proposition/negation (index18513 = i)), F index18513 = 0)
  → signed/expr-sum-value F n = F i

signed/unit-mass-selected-others-zero :
  (F : ℕ → ℚ) (n : ℕ)
  (nonnegative : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ F idx)
  (unit : signed/expr-sum-value F n = 1)
  (i : ℕ) (hi : nat/strict-below i n)
  (selected : F i = 1)
  (j : ℕ) (hj : nat/strict-below j n) (distinct : proposition/negation (i = j))
  → F j = 0

signed/expr-sum-complements :
  (F : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun index18543 => 1 + signed/negate (F index18543)) n = signed/from-nnrat (nnrat/make n 0) + signed/negate (signed/expr-sum-value F n)

signed/all-but-one-unit-capacity-saturated :
  (F : ℕ → ℚ) (q : ℕ)
  (upper : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ q)), F idx ≤ 1)
  (total : signed/expr-sum-value F (data/succ q) = signed/from-nnrat (nnrat/make q 0))
  (i : ℕ) (hi : nat/strict-below i (data/succ q))
  (zero : F i = 0)
  (j : ℕ) (hj : nat/strict-below j (data/succ q))
  (distinct : proposition/negation (i = j))
  → F j = 1

signed/all-but-one-ones-sum :
  (F : ℕ → ℚ) (q i : ℕ) (hi : nat/strict-below i (data/succ q))
  (zero : F i = 0)
  (others : ∀ (index18556 : ℕ), ∀ (bound18557 : nat/strict-below index18556 (data/succ q)), ∀ (distinct18558 : proposition/negation (index18556 = i)), F index18556 = 1)
  → signed/expr-sum-value F (data/succ q) = signed/from-nnrat (nnrat/make q 0)