BidVector

formal source

 101/-! ## §1. The auction setup -/
 102
 103/-- A bid vector for `n` agents. -/
 104abbrev BidVector (n : ℕ) := Fin n → ℝ
 105
 106/-! ## §2. Two-agent VCG (the cleanest non-trivial case)
 107
 108We prove DSIC in full for two agents. The argument generalizes
 109immediately to `n` agents (the runner-up is just the second-highest
 110bid in `Finset.image b Finset.univ.erase i*`), but two agents capture
 111the σ-conservation structure with no combinatorial overhead.
 112
 113Agent 0 vs. Agent 1. Each has a private valuation `v₀, v₁ ≥ 0` and
 114submits a bid `b₀, b₁ ∈ ℝ`. The high bidder wins (ties broken
 115arbitrarily — we break to agent 0). The winner pays the loser's bid;
 116the loser pays nothing.
 117-/
 118
 119/-- The winner under bid pair `(b₀, b₁)`. Returns `0` if `b₀ ≥ b₁`,
 120else `1`. -/
 121def winner (b₀ b₁ : ℝ) : Fin 2 :=
 122  if b₀ ≥ b₁ then 0 else 1
 123
 124/-- The payment by agent `0` under bid pair `(b₀, b₁)`. Equals `b₁`
 125if 0 wins, else 0. -/
 126def payment₀ (b₀ b₁ : ℝ) : ℝ :=
 127  if b₀ ≥ b₁ then b₁ else 0
 128
 129/-- The payment by agent `1` under bid pair `(b₀, b₁)`. Equals `b₀`
 130if 1 wins, else 0. -/
 131def payment₁ (b₀ b₁ : ℝ) : ℝ :=
 132  if b₀ ≥ b₁ then 0 else b₀
 133
 134/-- Agent 0's utility under valuation `v₀` and bid pair `(b₀, b₁)`. -/