Prove2Me

(5), p. 19 and OA p. 13 — the PU cutoff exceeds the PP cutoff

Proved
PersPricingDist.PersonalA.cutoff_order

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

dual-distributionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1personalized-pricingthreshold

For every s∈(0,1)s\in(0,1), the PU valuation cutoff is strictly larger than the PP cutoff:

v~(s)<vˇ(s).\tilde v(s)<\check v(s).

The inequality identifies the larger range of markets in which mono distribution remains optimal when B must charge a uniform price.

Preamble
import Mathlib
import Definitions.Def_PersPricingDist_PersonalA_Setting
Formal statement
namespace PersPricingDist.PersonalA

theorem cutoff_order :
    ∀ s ∈ Set.Ioo (0 : ℝ) 1, Model.vTilde s < Model.vCheck s := by sorry

end PersPricingDist.PersonalA
Source
Jullien, Reisinger & Rey, authors' manuscript of March 2022 (doi:10.1287/mnsc.2022.4437; PDF sha256 25a6c84a…c253), p. 19, (5) (PDF 21); OA p. 13 (PDF 46)
Human review

  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 16, 2026

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

View graph