Reference · Finite sums

rainbow.math.sums.indicator-zero

Finite sumssrc/rainbow/math/sums/indicator_zero.clj0 definitions, 4 theorems

A zero sum of strict-violation indicators means every weak inequality holds.

Depends onmath.sums.strict-indicatormath.sums.binary-conflicts

signed/zero-strict-indicator-implies-order :
  (x y : ℚ)
  (zero : data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x y) = 0)
  → x ≤ y

signed/order-implies-zero-strict-indicator :
  (x y : ℚ)
  (order : x ≤ y)
  → data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x y) = 0

signed/zero-strict-indicator-sum-implies-orders :
  (F G : ℕ → ℚ) (n : ℕ)
  (sum : signed/expr-sum-value (fun index16571 => data/Bool.rec (fun x₆ => ℚ) 1 0 (signed/decide-at-most (F index16571) (G index16571))) n ≤ 0)
  (idx : ℕ) (bound : nat/strict-below idx n)
  → F idx ≤ G idx

signed/orders-imply-zero-strict-indicator-sum :
  (F G : ℕ → ℚ) (n : ℕ)
  (orders : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  → signed/expr-sum-value (fun index16579 => data/Bool.rec (fun x₆ => ℚ) 1 0 (signed/decide-at-most (F index16579) (G index16579))) n ≤ 0