payment

formal source

 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₁)`. -/
 135def utility₀ (v₀ b₀ b₁ : ℝ) : ℝ :=
 136  if b₀ ≥ b₁ then v₀ - b₁ else 0
 137
 138/-- Agent 1's utility under valuation `v₁` and bid pair `(b₀, b₁)`. -/
 139def utility₁ (v₁ b₀ b₁ : ℝ) : ℝ :=
 140  if b₀ ≥ b₁ then 0 else v₁ - b₀
 141
 142/-! ## §3. DSIC for agent 0 -/
 143
 144/-- **DSIC for agent 0.** For any opposing bid `b₁`, agent 0 cannot
 145strictly improve their utility by bidding any `b₀'` other than their
 146true valuation `v₀`. -/
 147theorem dsic_agent_zero (v₀ b₁ : ℝ) (b₀' : ℝ) :
 148    utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁ := by
 149  unfold utility₀
 150  by_cases h_truth : v₀ ≥ b₁
 151  · -- Truthful: agent 0 wins, utility = v₀ - b₁ ≥ 0.
 152    rw [if_pos h_truth]
 153    by_cases h_dev : b₀' ≥ b₁
 154    · -- Deviation also wins, utility = v₀ - b₁ (same).
 155      rw [if_pos h_dev]
 156    · -- Deviation loses, utility = 0 ≤ v₀ - b₁.