Reference · Finite sums

rainbow.math.sums.one-hot-factor

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

Reusable selection factorization for arbitrary signed values. Only the inner selector is one-hot; the outer weights may have any sign or total. Bridges to the existing selector and operation-preservation theorem, with no new induction.

signed/expr-sum-one-hot-product :
  (oh-B oh-F oh-G : ℕ → ℚ) (oh-n : ℕ)
  (oh-bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx oh-n), oh-B idx · (1 + signed/negate (oh-B idx)) = 0)
  (oh-unit : signed/expr-sum-value oh-B oh-n = 1)
  → signed/expr-sum-value (fun oh-v => oh-B oh-v · (fun oh-v₁ => oh-F oh-v₁ · oh-G oh-v₁) oh-v) oh-n = signed/expr-sum-value (fun oh-v => oh-B oh-v · oh-F oh-v) oh-n · signed/expr-sum-value (fun oh-v => oh-B oh-v · oh-G oh-v) oh-n

signed/expr-sum-one-hot-right-factor :
  (oh-A oh-B oh-F : ℕ → ℚ) (oh-G : ℕ → ℕ → ℚ) (oh-m oh-n : ℕ)
  (oh-bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx oh-n), oh-B idx · (1 + signed/negate (oh-B idx)) = 0)
  (oh-unit : signed/expr-sum-value oh-B oh-n = 1)
  → signed/expr-sum-value (fun oh-u => oh-A oh-u · signed/expr-sum-value (fun oh-v => oh-B oh-v · (fun oh-v₁ => (fun oh-u₁ => fun oh-v₂ => oh-F oh-v₂ · oh-G oh-u₁ oh-v₂) oh-u oh-v₁) oh-v) oh-n) oh-m = signed/expr-sum-value (fun oh-v => oh-B oh-v · oh-F oh-v) oh-n · signed/expr-sum-value (fun oh-u => oh-A oh-u · signed/expr-sum-value (fun oh-v => oh-B oh-v · (fun oh-v₁ => oh-G oh-u oh-v₁) oh-v) oh-n) oh-m