Lemma 2 (proof of Proposition 4) — $\max\{\tilde b, L\}$ maximizes $u^+$ on $[L,\infty)$

Proved

RobustFPA.VarBid.lemma_2

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

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

Let $n \ge 2$ , $0 < \tau < 1$ and $L < v$ . With $p(b) = (b-L)/(v-L)$ , $u^+(b) = (v-b)(1-\tau+\tau p(b))^{n-1}$ and $\tilde b = v - (v-L)/(n\tau)$ ,

\max\{\tilde b, L\} \in \arg\sup_{\hat b \ge L} u^+(\hat b),

that is, $\max\{\tilde b, L\} \ge L$ and $u^+(\hat b) \le u^+(\max\{\tilde b, L\})$ for every $\hat b \ge L$ .

The lemma identifies the best response to the worst case for bidding too high, in which all unconstrained opponents bid $L$ ; it is the first step in reducing the set $X$ of Proposition 3 to the solutions of Equation (3).

Formalization Note. $u^+$ is the polynomial of the ClosedForms file on all of $\mathbb R$ ; for $\hat b > v$ it is negative, so the supremum over $[L, \infty)$ is the paper's.

Preamble

import Mathlib
import Definitions.Def_RobustFPA_VarBid_ClosedForms

Formal statement

namespace RobustFPA.VarBid

theorem lemma_2 (n : ℕ) (hn : 2 ≤ n) (τ L v : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) (hLv : L < v) :
    L ≤ max (bTilde n τ L v) L ∧
    ∀ b : ℝ, L ≤ b → uPlus n τ L v b ≤ uPlus n τ L v (max (bTilde n τ L v) L) := by sorry

end RobustFPA.VarBid

Source

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

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

Lemma 2 (proof of Proposition 4) — max⁡{b~,L}\max\{\tilde b, L\}max{b~,L} maximizes u+u^+u+ on [L,∞)[L,\infty)[L,∞)

Lemma 2 (proof of Proposition 4) — $\max\{\tilde b, L\}$ maximizes $u^+$ on $[L,\infty)$