theorem
proved
tactic proof
sigma_conservation_truthful
show as:
view Lean formalization →
formal statement (Lean)
216theorem sigma_conservation_truthful (v₀ v₁ : ℝ) :
217 utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
218 (payment₀ v₀ v₁ + payment₁ v₀ v₁)
219 = max v₀ v₁ := by
proof body
Tactic-mode proof.
220 unfold utility₀ utility₁ payment₀ payment₁
221 by_cases h : v₀ ≥ v₁
222 · -- Agent 0 wins. utility₀ = v₀ - v₁, utility₁ = 0, payment₀ = v₁, payment₁ = 0.
223 -- Sum = (v₀ - v₁) + 0 + v₁ + 0 = v₀ = max v₀ v₁ (since v₀ ≥ v₁).
224 rw [if_pos h, if_pos h, if_pos h, if_pos h]
225 rw [max_eq_left h]
226 ring
227 · -- Agent 1 wins. utility₀ = 0, utility₁ = v₁ - v₀, payment₀ = 0, payment₁ = v₀.
228 -- Sum = 0 + (v₁ - v₀) + 0 + v₀ = v₁ = max v₀ v₁ (since v₁ > v₀).
229 push_neg at h
230 have h_le : v₀ ≤ v₁ := le_of_lt h
231 have h_not : ¬ (v₀ ≥ v₁) := by linarith
232 rw [if_neg h_not, if_neg h_not, if_neg h_not, if_neg h_not]
233 rw [max_eq_right h_le]
234 ring
235
236/-- **WELFARE OPTIMALITY.** The VCG allocation maximizes social welfare:
237the agent with the higher valuation gets the item under truthful
238bidding. -/