Prove2Me

Proof of Proposition 4, p. 49 — XX is exactly the set of solutions of Equation (3) in [max⁡{L,b~},v1][\max\{L,\tilde b\}, v_1]

Proved
RobustFPA.VarBid.equalizerSet_eq

by mikedeng1 · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

first-price-auctionminimax-lossp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let n≥2n \ge 2, 0<τ<10 < \tau < 1 and L<vL < v, with GG uniform on [L,v][L, v]. The set XX of Proposition 3 consists exactly of the bids in [max⁡{L,b~},v][\max\{L,\tilde b\}, v] that solve Equation (3):

X={b:max⁡{L,b~}≤b≤v,  u+(max⁡{L,b~})−u+(b)=u+(b)−u−(b)}.X = \Bigl\{ b : \max\{L,\tilde b\} \le b \le v,\ \ u^+(\max\{L,\tilde b\}) - u^+(b) = u^+(b) - u^-(b) \Bigr\}.

In particular no bid in [L,max⁡{L,b~})[L, \max\{L, \tilde b\}) equalizes the two maximal losses.

On [max⁡{L,b~},v][\max\{L,\tilde b\}, v] the maximal loss of bidding too high is u+(max⁡{L,b~})−u+(b)u^+(\max\{L,\tilde b\}) - u^+(b) and that of bidding too low is u+(b)−u−(b)u^+(b) - u^-(b); below the peak the too-high loss vanishes while the too-low loss is positive. This is the step that turns Proposition 3 into Equation (3).

Formalization Note. Both sides are sets of reals; XX is defined by the two suprema of Proposition 3, not by Equation (3), so the identity has content.

Preamble
import Mathlib
import Definitions.Def_RobustFPA_VarBid_ClosedForms
Formal statement
namespace RobustFPA.VarBid

theorem equalizerSet_eq (n : ℕ) (hn : 2 ≤ n) (τ L v : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) (hLv : L < v) :
    equalizerSet n τ L v = {b | peakBid n τ L v ≤ b ∧ b ≤ v ∧ Equation3 n τ L v b} := by sorry

end RobustFPA.VarBid
Source
Kasberger & Schlag, Robust Bidding in First-Price Auctions, SSRN 3044438 (version of 3 Sep 2022), p. 49 (Appendix B.4, proof of Proposition 4, after Lemma 2)
Human review

  • Endorsed by Shuze Chen · Oct 20, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 20, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph