Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.vickrey-dsic

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/vickrey_dsic.clj0 definitions, 5 theorems

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

signed/vickrey-others-lose :
  (w : ℕ → ℚ) (n : ℕ)
  (hw01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx · (1 + signed/negate (w idx)) = 0)
  (hsum : signed/expr-sum-value (fun ws => w ws) n = 1)
  (i : ℕ) (i-lt : nat/strict-below i n)
  (hwi : w i = 1)
  (j : ℕ) (j-lt : nat/strict-below j n) (hne : proposition/negation (j = i))
  → w j = 0

signed/vickrey-winner-bid :
  (b w : ℕ → ℚ) (n : ℕ)
  (hw01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx · (1 + signed/negate (w idx)) = 0)
  (hsum : signed/expr-sum-value (fun ws => w ws) n = 1)
  (i : ℕ) (i-lt : nat/strict-below i n)
  (hwi : w i = 1)
  → signed/expr-sum-value (fun wb => w wb · b wb) n = b i

signed/vickrey-price-bound :
  (b w : ℕ → ℚ) (p : ℚ) (n : ℕ)
  (hw01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx · (1 + signed/negate (w idx)) = 0)
  (hatt : 1 ≤ signed/expr-sum-value (fun ai => (1 + signed/negate (w ai)) · (data/Bool.rec (fun x₉ => ℚ) 0 1 (signed/decide-at-most (b ai) p) · data/Bool.rec (fun x₁₂ => ℚ) 0 1 (signed/decide-at-most p (b ai)))) n)
  (R : ℚ)
  (hR : ∀ (rj : ℕ), ∀ (rj-lt : nat/strict-below rj n), ∀ (rz : w rj = 0), b rj ≤ R)
  → p ≤ R

signed/vickrey-others-below-price :
  (b w : ℕ → ℚ) (p : ℚ) (n : ℕ)
  (hw01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w idx · (1 + signed/negate (w idx)) = 0)
  (hsum : signed/expr-sum-value (fun ws => w ws) n = 1)
  (hlose : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), (1 + signed/negate (w idx)) · b idx ≤ p)
  (i : ℕ) (i-lt : nat/strict-below i n)
  (hwi : w i = 1)
  (j : ℕ) (j-lt : nat/strict-below j n) (hne : proposition/negation (j = i))
  → b j ≤ p

signed/vickrey-truthful-dominant :
  (b1 w1 : ℕ → ℚ) (p1 : ℚ) (b2 w2 : ℕ → ℚ) (p2 : ℚ) (n : ℕ)
  (h1w01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w1 idx · (1 + signed/negate (w1 idx)) = 0)
  (h1sum : signed/expr-sum-value (fun ws => w1 ws) n = 1)
  (h1win : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), b1 idx ≤ signed/expr-sum-value (fun wb => w1 wb · b1 wb) n)
  (h1lose : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), (1 + signed/negate (w1 idx)) · b1 idx ≤ p1)
  (h1att : 1 ≤ signed/expr-sum-value (fun ai => (1 + signed/negate (w1 ai)) · (data/Bool.rec (fun x₉ => ℚ) 0 1 (signed/decide-at-most (b1 ai) p1) · data/Bool.rec (fun x₁₂ => ℚ) 0 1 (signed/decide-at-most p1 (b1 ai)))) n)
  (h2w01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), w2 idx · (1 + signed/negate (w2 idx)) = 0)
  (h2sum : signed/expr-sum-value (fun ws => w2 ws) n = 1)
  (h2win : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), b2 idx ≤ signed/expr-sum-value (fun wb => w2 wb · b2 wb) n)
  (h2lose : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), (1 + signed/negate (w2 idx)) · b2 idx ≤ p2)
  (h2att : 1 ≤ signed/expr-sum-value (fun ai => (1 + signed/negate (w2 ai)) · (data/Bool.rec (fun x₂₁ => ℚ) 0 1 (signed/decide-at-most (b2 ai) p2) · data/Bool.rec (fun x₂₄ => ℚ) 0 1 (signed/decide-at-most p2 (b2 ai)))) n)
  (i : ℕ) (i-lt : nat/strict-below i n)
  (hsame : ∀ (sj : ℕ), ∀ (sj-lt : nat/strict-below sj n), ∀ (sne : proposition/negation (sj = i)), b1 sj = b2 sj)
  → w2 i · (b1 i + signed/negate p2) ≤ w1 i · (b1 i + signed/negate p1)