Prove2Me

Section A.5 — C[x∗]=NN+1(c0vˉ)N+1pp+N+1C[x^*]=\frac N{N+1}(c_0\bar v)^{N+1}\frac p{p+N+1}

Proved
GradedReserve.candidate_loss

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

auctionsbayes-nash-equilibriummechanism-designp2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-guarantee

Let F(v)=vkF(v)=v^k (k≥1k\ge1 real), n≥2n\ge2 and p>pmin⁡p>p_{\min}. The anchored loss of the candidate is

C[x∗]=NN+1 (c0vˉ)N+1 pp+N+1.C[x^*]=\frac N{N+1}\,(c_0\bar v)^{N+1}\,\frac p{p+N+1}.

With (25) this gives the optimal anchored revenue NN+1[1−b0N+1pp+N+1]\frac N{N+1}\big[1-b_0^{N+1}\frac p{p+N+1}\big] of Theorem 3.1.

Differences from the source:

  • encoding: F(v) = v^k with k ≥ 1 → powerDensity k (density k v^{k−1} on [0,1]); k real, Real.rpow; reason: the same law for every real k ≥ 1
Preamble
import Mathlib
import Definitions.Def_GradedReserve_Cfun
import Definitions.Def_GradedReserve_cZero
import Definitions.Def_GradedReserve_pMin
import Definitions.Def_GradedReserve_powN
import Definitions.Def_GradedReserve_vbar
import Definitions.Def_GradedReserve_xStar
open MeasureTheory ProbabilityTheory Set Filter Topology
Formal statement
namespace GradedReserve

/-- **The candidate's anchored loss** (Chen–Wang, *Optimal Auctions for Anchored Bidders under a Rational Revenue Guarantee*, manuscript (STOC 2027 submission), Section A.5, p.19, PDF 20): direct integration gives
`C[x*] = (N/(N+1)) (c₀ v̄)^{N+1} p/(p+N+1)` for `p > p_min`. -/
theorem candidate_loss (k : ℝ) (hk : 1 ≤ k) (n : ℕ) (hn : 2 ≤ n) (p : ℝ) (hp : pMin k n < p) :
    Cfun k n (xStar k n p) =
      powN k n / (powN k n + 1) * (cZero k n p * vbar k n p) ^ (powN k n + 1)
        * (p / (p + powN k n + 1)) := by sorry

end GradedReserve
Source
Chen–Wang, Optimal Auctions for Anchored Bidders under a Rational Revenue Guarantee, manuscript (STOC 2027 submission; PDF sha256 6b1da440…1bab), Section A.5, p.19 (PDF 20)
Human review

  • Endorsed by Shuze Chen · Nov 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 6, 2026

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

View graph