Reference · Finite sums

rainbow.math.sums.predicate-bridges

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

Reusable bridges from checker indicators and squared norms to mathematical predicates.

Depends onmath.sums.lp-boundsmath.sums.nonneg-zeromath.linear.vector.norm-nonnegativemath.rational.signed.square-zeromath.rational.signed.strict-ordermath.rational.signed.decide-completeness

signed/positive-implies-indicator-one :
  (x : ℚ)
  (positive : 0 < x)
  → 1 ≤ data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x 0)

signed/positive-square-sum-implies-nonzero :
  (v : ℕ → ℚ) (n : ℕ)
  (positive : 0 < signed/expr-sum-value (fun square18454 => v square18454 · v square18454) n)
  → proposition/negation (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), v idx = 0)

signed/nonzero-implies-positive-square-sum :
  (v : ℕ → ℚ) (n : ℕ)
  (nonzero : proposition/negation (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), v idx = 0))
  → 0 < signed/expr-sum-value (fun square18457 => v square18457 · v square18457) n