Reference · Finite sums

rainbow.math.sums.zero-violations

Finite sumssrc/rainbow/math/sums/zero_violations.clj0 definitions, 8 theorems

Zero positive-part penalties mean no violated inequality; a minimum encodes disjunction.

Depends onmath.sums.binary-conflictsmath.rational.signed.decide-order

signed/positive-part-zero-of-nonpositive :
  (x : ℚ)
  (nonpositive : x ≤ 0)
  → data/Bool.rec (fun x₄ => ℚ) 0 x (signed/decide-at-most 0 x) = 0

signed/nonpositive-of-positive-part-zero :
  (x : ℚ)
  (zero : data/Bool.rec (fun x₄ => ℚ) 0 x (signed/decide-at-most 0 x) = 0)
  → x ≤ 0

signed/nonpositive-minimum-implies-disjunction :
  (x y : ℚ)
  (nonpositive : data/Bool.rec (fun x₄ => ℚ) y x (signed/decide-at-most x y) ≤ 0)
  → proposition/disjunction (x ≤ 0) (y ≤ 0)

signed/disjunction-implies-nonpositive-minimum :
  (x y : ℚ) (either : proposition/disjunction (x ≤ 0) (y ≤ 0))
  → data/Bool.rec (fun x₄ => ℚ) y x (signed/decide-at-most x y) ≤ 0

signed/nonpositive-difference-implies-at-most :
  (x y : ℚ)
  (difference : x + signed/negate y ≤ 0)
  → x ≤ y

signed/at-most-implies-nonpositive-difference :
  (x y : ℚ)
  (ordered : x ≤ y)
  → x + signed/negate y ≤ 0

signed/zero-penalty-sum-implies-constraints :
  (W V : ℕ → ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (sum : signed/expr-sum-value (fun entry16712 => W entry16712 · data/Bool.rec (fun x₄ => ℚ) 0 (V entry16712) (signed/decide-at-most 0 (V entry16712))) n ≤ 0)
  (entry16713 : ℕ) (bound16714 : nat/strict-below entry16713 n)
  (selected16715 : W entry16713 = 1)
  → V entry16713 ≤ 0

signed/constraints-imply-zero-penalty-sum :
  (W V : ℕ → ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (constraints : ∀ (entry16721 : ℕ), ∀ (bound16722 : nat/strict-below entry16721 n), ∀ (selected16723 : W entry16721 = 1), V entry16721 ≤ 0)
  → signed/expr-sum-value (fun entry16720 => W entry16720 · data/Bool.rec (fun x₄ => ℚ) 0 (V entry16720) (signed/decide-at-most 0 (V entry16720))) n ≤ 0