def definition def or abbrev

`utility`

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

formal statement (Lean)

 135def utility₀ (v₀ b₀ b₁ : ℝ) : ℝ :=

proof body

Definition body.

 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₀`. -/