Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.borda

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/borda.clj0 definitions, 7 theorems

General lemmas: borda. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/eq-indicator-one-of-equivalent :
  (p c : ℚ)
  (h : p = c)
  → data/Bool.rec (fun x₄ => ℚ) 0 1 (signed/decide-at-most p c) · data/Bool.rec (fun x₈ => ℚ) 0 1 (signed/decide-at-most c p) = 1

signed/equivalent-of-eq-indicator-one :
  (p c : ℚ)
  (h : data/Bool.rec (fun x₄ => ℚ) 0 1 (signed/decide-at-most p c) · data/Bool.rec (fun x₈ => ℚ) 0 1 (signed/decide-at-most c p) = 1)
  → p = c

signed/unit-sum-witness :
  (F : ℕ → ℚ) (k : ℕ)
  (h01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx k), proposition/disjunction (F idx = 0) (F idx = 1))
  (hsum : signed/expr-sum-value F k = 1)
  → proposition/existence ℕ (fun wi => proposition/conjunction (nat/strict-below wi k) (F wi = 1))

signed/eq-indicator-zero-or-one :
  (p c : ℚ)
  → proposition/disjunction (data/Bool.rec (fun x₂₀ => ℚ) 0 1 (signed/decide-at-most p c) · data/Bool.rec (fun x₂₄ => ℚ) 0 1 (signed/decide-at-most c p) = 0) (data/Bool.rec (fun x₂₈ => ℚ) 0 1 (signed/decide-at-most p c) · data/Bool.rec (fun x₃₂ => ℚ) 0 1 (signed/decide-at-most c p) = 1)

signed/less-than-add-one :
  (x : ℚ)
  → x < x + 1

signed/of-nat-strictly-increasing :
  (K lk : ℕ) (lk-lt : nat/strict-below lk K)
  → signed/from-nnrat (nnrat/make lk 0) < signed/from-nnrat (nnrat/make K 0)

signed/literal-indicators-at-most-one :
  (x : ℚ) (K : ℕ)
  → signed/expr-sum-value (fun ik => data/Bool.rec (fun x₉ => ℚ) 0 1 (signed/decide-at-most x (signed/from-nnrat (nnrat/make ik 0))) · data/Bool.rec (fun x₁₂ => ℚ) 0 1 (signed/decide-at-most (signed/from-nnrat (nnrat/make ik 0)) x)) K ≤ 1