utility

formal source

 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₁.
 157      rw [if_neg h_dev]
 158      linarith
 159  · -- Truthful: agent 0 loses, utility = 0.
 160    rw [if_neg h_truth]
 161    by_cases h_dev : b₀' ≥ b₁
 162    · -- Deviation wins, utility = v₀ - b₁ < 0.
 163      rw [if_pos h_dev]
 164      push_neg at h_truth
 165      linarith