254theorem truthful_is_nash (v₀ v₁ : ℝ) : 255 -- (1) Agent 0 cannot improve by deviating from v₀ given agent 1 plays v₁. 256 (∀ b₀' : ℝ, utility₀ v₀ b₀' v₁ ≤ utility₀ v₀ v₀ v₁) ∧ 257 -- (2) Agent 1 cannot improve by deviating from v₁ given agent 0 plays v₀. 258 (∀ b₁' : ℝ, utility₁ v₁ v₀ b₁' ≤ utility₁ v₁ v₀ v₁) :=
proof body
Term-mode proof.
259 ⟨dsic_agent_zero v₀ v₁, dsic_agent_one v₁ v₀⟩ 260 261/-! ## §6. Sigma-cost as the payment formula 262 263In RS terms, the σ-cost of running the auction is the externality 264the winner imposes on the runner-up. The VCG payment formula 265**equals** that σ-cost. This is the operational meaning of 266"σ-conserving auction": the payment is the σ-cost. 267-/ 268 269/-- The σ-cost of allocating the item to agent 0 when agent 1 had 270valuation v₁: agent 1 loses out on utility `v₁` they would have got 271in the counterfactual where agent 0 was absent. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.