Reference · Finite sums

rainbow.math.sums.one-hot-pair

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

Two independent one-hot rows select exactly the corresponding matrix entry.

Depends onmath.sums.one-hot-value

signed/one-hot-bilinear-implies-selected-pair-values :
  (W Z : ℕ → ℚ) (D : ℕ → ℕ → ℚ) (V : ℚ) (m n : ℕ)
  (wb : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), proposition/disjunction (W idx = 0) (W idx = 1))
  (wu : signed/expr-sum-value W m = 1)
  (zb : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (Z idx = 0) (Z idx = 1))
  (zu : signed/expr-sum-value Z n = 1)
  (value : V = signed/expr-sum-value (fun z => W z · (fun row17553 => signed/expr-sum-value (fun z₁ => Z z₁ · D row17553 z₁) n) z) m)
  (row17554 : ℕ) (bound17555 : nat/strict-below row17554 m)
  (selected17556 : W row17554 = 1)
  (column17557 : ℕ) (bound17558 : nat/strict-below column17557 n)
  (selected17559 : Z column17557 = 1)
  → V = D row17554 column17557

signed/selected-pair-values-imply-one-hot-bilinear :
  (W Z : ℕ → ℚ) (D : ℕ → ℕ → ℚ) (V : ℚ) (m n : ℕ)
  (wb : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), proposition/disjunction (W idx = 0) (W idx = 1))
  (wu : signed/expr-sum-value W m = 1)
  (zb : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (Z idx = 0) (Z idx = 1))
  (zu : signed/expr-sum-value Z n = 1)
  (values : ∀ (row17568 : ℕ), ∀ (bound17569 : nat/strict-below row17568 m), ∀ (selected17570 : W row17568 = 1), ∀ (column17571 : ℕ), ∀ (bound17572 : nat/strict-below column17571 n), ∀ (selected17573 : Z column17571 = 1), V = D row17568 column17571)
  → V = signed/expr-sum-value (fun z => W z · (fun row17567 => signed/expr-sum-value (fun z₁ => Z z₁ · D row17567 z₁) n) z) m