Reference · Finite sums

rainbow.math.sums.one-hot-value

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

Pointwise values of a selected index, their weighted equality, and explicit attainment.

Depends onmath.sums.one-hot-index

signed/one-hot-value-implies-selected-values :
  (W F : ℕ → ℚ) (V : ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (unit : signed/expr-sum-value W n = 1)
  (value : V = signed/expr-sum-value (fun z => W z · F z) n)
  (selected-index17519 : ℕ) (bound17520 : nat/strict-below selected-index17519 n)
  (selected17521 : W selected-index17519 = 1)
  → V = F selected-index17519

signed/selected-values-imply-one-hot-value :
  (W F : ℕ → ℚ) (V : ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (unit : signed/expr-sum-value W n = 1)
  (values : ∀ (selected-index17525 : ℕ), ∀ (bound17526 : nat/strict-below selected-index17525 n), ∀ (selected17527 : W selected-index17525 = 1), V = F selected-index17525)
  → V = signed/expr-sum-value (fun z => W z · F z) n

signed/one-hot-value-is-attained :
  (W F : ℕ → ℚ) (V : ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (unit : signed/expr-sum-value W n = 1)
  (value : V = signed/expr-sum-value (fun z => W z · F z) n)
  → proposition/existence ℕ (fun index => proposition/conjunction (nat/strict-below index n) (F index = V))