Prove2Me

Proof of Proposition 4, p. 51 — the root of Equation (3) strictly increases from nn to n+1n+1 bidders

Proved
RobustFPA.VarBid.root_increasing

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

comparative-staticsfirst-price-auctionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let n≥2n \ge 2, 0<τ<10 < \tau < 1 and L<vL < v. Write un+u^+_n, un−u^-_n, b~n\tilde b_n for the functions of the ClosedForms file with nn bidders. If bb solves Equation (3) for nn bidders on [max⁡{L,b~n},v][\max\{L,\tilde b_n\}, v],

un+(max⁡{L,b~n})−un+(b)=un+(b)−un−(b),u^+_n(\max\{L,\tilde b_n\}) - u^+_n(b) = u^+_n(b) - u^-_n(b),

and b′b' solves Equation (3) for n+1n+1 bidders on [max⁡{L,b~n+1},v][\max\{L,\tilde b_{n+1}\}, v], then

b<b′.b < b'.

This is the comparative statics part of Proposition 4: the minimax loss bid shades less as competition grows.

Formalization Note. The paper differentiates the root E(b,n)=0E(b,n) = 0 in a real-valued nn via the implicit function theorem; the statement here is the integer comparison between nn and n+1n+1 bidders, which is what "increases in the number of bidders" means. The increase is strict, as in the paper's ∂E/∂n<0\partial E/\partial n < 0. Same τ\tau, LL, vv for both nn and n+1n+1.

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

theorem root_increasing (n : ℕ) (hn : 2 ≤ n) (τ L v : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) (hLv : L < v) (b b' : ℝ)
    (hb : peakBid n τ L v ≤ b ∧ b ≤ v ∧ Equation3 n τ L v b)
    (hb' : peakBid (n + 1) τ L v ≤ b' ∧ b' ≤ v ∧ Equation3 (n + 1) τ L v b') :
    b < b' := by sorry

end RobustFPA.VarBid
Source
Kasberger & Schlag, Robust Bidding in First-Price Auctions, SSRN 3044438 (version of 3 Sep 2022), p. 51 (Appendix B.4, proof of Proposition 4: the minimax loss bid increases in n)
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