winner

formal source

 118
 119/-- The winner under bid pair `(b₀, b₁)`. Returns `0` if `b₀ ≥ b₁`,
 120else `1`. -/
 121def winner (b₀ b₁ : ℝ) : Fin 2 :=
 122  if b₀ ≥ b₁ then 0 else 1
 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.