pith. machine review for the scientific record. sign in
theorem proved term proof

welfare_optimal_truthful

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 239theorem welfare_optimal_truthful (v₀ v₁ : ℝ) :
 240    -- The winner's valuation equals the maximum.
 241    (winner v₀ v₁ = 0 ∧ v₀ ≥ v₁) ∨ (winner v₀ v₁ = 1 ∧ v₀ < v₁) := by

proof body

Term-mode proof.

 242  unfold winner
 243  by_cases h : v₀ ≥ v₁
 244  · exact Or.inl ⟨if_pos h, h⟩
 245  · push_neg at h
 246    refine Or.inr ⟨?_, h⟩
 247    rw [if_neg (by linarith : ¬ v₀ ≥ v₁)]
 248
 249/-! ## §5. Truthful bidding is a Nash equilibrium -/
 250
 251/-- **TRUTHFUL BIDDING IS A NASH EQUILIBRIUM.** No agent gains by
 252unilaterally deviating from truthful bidding. (This is weaker than
 253DSIC, but is the standard solution-concept statement.) -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.