Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.weighted-median

Lemmas behind operations-research checks src/rainbow/math/lemmas/weighted_median.clj0 definitions, 11 theorems

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

signed/difference-at-most-reverse

TheoremFor all inputsNo axiomsSource

signed/difference-at-most-reverse :
  (u v : ℚ)
  (h : u ≤ v)
  → u + signed/negate v ≤ v + signed/negate u

+ = signed/addℚ = signed/SignedRational≤ = signed/at-most

signed/decided-abs-at-least-difference

TheoremFor all inputsNo axiomsSource

signed/decided-abs-at-least-difference :
  (p x : ℚ)
  → p + signed/negate x ≤ data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x)

+ = signed/addℚ = signed/SignedRational≤ = signed/at-most

signed/decided-abs-at-least-reverse-difference

TheoremFor all inputsNo axiomsSource

signed/decided-abs-at-least-reverse-difference :
  (p x : ℚ)
  → x + signed/negate p ≤ data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x)

+ = signed/addℚ = signed/SignedRational≤ = signed/at-most

signed/decided-abs-when-left

TheoremFor all inputsNo axiomsSource

signed/decided-abs-when-left :
  (p x : ℚ)
  (h : p ≤ x)
  → data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x) = x + signed/negate p

+ = signed/add= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most

signed/decided-abs-when-right

TheoremFor all inputsNo axiomsSource

signed/decided-abs-when-right :
  (p x : ℚ)
  (h : x ≤ p)
  → data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x) = p + signed/negate x

+ = signed/add= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most

signed/abs-shift-right

TheoremFor all inputsNo axiomsSource

signed/abs-shift-right :
  (p x y : ℚ)
  → data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x) + (y + signed/negate x) + signed/negate (data/Bool.rec (fun x₈ => ℚ) 1 0 (signed/decide-at-most p x) · (y + signed/negate x + (y + signed/negate x))) ≤ data/Bool.rec (fun x₁₂ => ℚ) (p + signed/negate y) (y + signed/negate p) (signed/decide-at-most p y)

+ = signed/add0 = signed/zero1 = signed/one· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most

signed/abs-shift-left

TheoremFor all inputsNo axiomsSource

signed/abs-shift-left :
  (p x y : ℚ)
  → data/Bool.rec (fun x₄ => ℚ) (p + signed/negate x) (x + signed/negate p) (signed/decide-at-most p x) + (x + signed/negate y) + signed/negate (data/Bool.rec (fun x₈ => ℚ) 1 0 (signed/decide-at-most x p) · (x + signed/negate y + (x + signed/negate y))) ≤ data/Bool.rec (fun x₁₂ => ℚ) (p + signed/negate y) (y + signed/negate p) (signed/decide-at-most p y)

+ = signed/add0 = signed/zero1 = signed/one· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most

signed/weighted-shift-expand

TheoremFor all inputsNo axiomsSource

signed/weighted-shift-expand :
  (w ab d i : ℚ)
  → w · (ab + d + signed/negate (i · (d + d))) = w · ab + w · d + signed/negate (i · w · (d + d))

+ = signed/add= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational

signed/median-gain

TheoremFor all inputsNo axiomsSource

signed/median-gain :
  (C W S d : ℚ)
  (hd : 0 ≤ d)
  (hs : signed/from-nnrat 2 · S ≤ W)
  → C ≤ C + W · d + signed/negate (S · (d + d))

+ = signed/add0 = signed/zero· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most

signed/weighted-abs-shift-sum

TheoremFor all inputsNo axiomsSource

signed/weighted-abs-shift-sum :
  (a w I : ℕ → ℚ) (x y d : ℚ) (n : ℕ)
  (hw : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ w idx)
  (hpt : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), data/Bool.rec (fun x₁ => ℚ) (a idx + signed/negate x) (x + signed/negate (a idx)) (signed/decide-at-most (a idx) x) + d + signed/negate (I idx · (d + d)) ≤ data/Bool.rec (fun x₂ => ℚ) (a idx + signed/negate y) (y + signed/negate (a idx)) (signed/decide-at-most (a idx) y))
  (hd : 0 ≤ d)
  (hside : signed/from-nnrat 2 · signed/expr-sum-value (fun si => I si · w si) n ≤ signed/expr-sum-value (fun tw => w tw) n)
  → signed/expr-sum-value (fun sa => w sa · data/Bool.rec (fun x₄ => ℚ) (a sa + signed/negate x) (x + signed/negate (a sa)) (signed/decide-at-most (a sa) x)) n ≤ signed/expr-sum-value (fun sy => w sy · data/Bool.rec (fun x₆ => ℚ) (a sy + signed/negate y) (y + signed/negate (a sy)) (signed/decide-at-most (a sy) y)) n

+ = signed/add0 = signed/zero· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/weighted-median-optimal

TheoremFor all inputsNo axiomsSource

signed/weighted-median-optimal :
  (a w : ℕ → ℚ) (x y C : ℚ) (n : ℕ)
  (hw : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ w idx)
  (hL : signed/from-nnrat 2 · signed/expr-sum-value (fun sw => data/Bool.rec (fun x₆ => ℚ) 1 0 (signed/decide-at-most x (a sw)) · w sw) n ≤ value)
  (hR : signed/from-nnrat 2 · signed/expr-sum-value (fun sw => data/Bool.rec (fun x₁₂ => ℚ) 1 0 (signed/decide-at-most (a sw) x) · w sw) n ≤ value)
  (hC : C = signed/expr-sum-value (fun cs => w cs · data/Bool.rec (fun x₁₄ => ℚ) (a cs + signed/negate x) (x + signed/negate (a cs)) (signed/decide-at-most (a cs) x)) n)
  → C ≤ signed/expr-sum-value (fun cs => w cs · data/Bool.rec (fun x₁₆ => ℚ) (a cs + signed/negate y) (y + signed/negate (a cs)) (signed/decide-at-most (a cs) y)) n
  where value := signed/expr-sum-value (fun tw => w tw) n

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most