Prove2Me

Proof of Proposition 4, p. 50 — Equation (3) has a unique solution in [max⁡{L,b~},v1][\max\{L,\tilde b\}, v_1]

Proved
RobustFPA.VarBid.equation3_unique

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

calculusfirst-price-auctionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let n≥2n \ge 2, 0<τ<10 < \tau < 1 and L<vL < v. On the interval I=[max⁡{L,b~},v]I = [\max\{L,\tilde b\}, v]:

  1. the left-hand side of Equation (3), b↦u+(max⁡{L,b~})−u+(b)b \mapsto u^+(\max\{L,\tilde b\}) - u^+(b), is nondecreasing;
  2. the right-hand side, b↦u+(b)−u−(b)b \mapsto u^+(b) - u^-(b), is strictly decreasing;
  3. Equation (3),
u+(max⁡{L,b~})−u+(b)=u+(b)−u−(b),u^+(\max\{L,\tilde b\}) - u^+(b) = u^+(b) - u^-(b),

has exactly one solution b∈Ib \in I.

Uniqueness of the root is what makes the minimax loss bid unique in Proposition 4.

Formalization Note. The page's bound "b>((n−1)+L)/nb > ((n-1)+L)/n" is a typo for ((n−1)v+L)/n((n-1)v+L)/n and is not part of the statement; only the monotonicity claims and the unique root are formalized. Strict decrease of the right-hand side uses τ<1\tau < 1 (p. 50, "which holds if and only if τ < 1").

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

theorem equation3_unique (n : ℕ) (hn : 2 ≤ n) (τ L v : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) (hLv : L < v) :
    MonotoneOn (fun b => uPlus n τ L v (peakBid n τ L v) - uPlus n τ L v b)
      (Set.Icc (peakBid n τ L v) v) ∧
    StrictAntiOn (fun b => uPlus n τ L v b - uMinus n τ L v b) (Set.Icc (peakBid n τ L v) 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), pp. 50–51 (Appendix B.4, proof of Proposition 4: uniqueness of the solution of Equation (3))
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