§6 — asymmetric optimal leader price and gross profits

Proved

PPDifferentiation.ShortRun.asymmetric_profits

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

hotellingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1personalized-pricingstackelberg-pricing

Suppose $t>0$ , $x_A<x_B$ , and $-2<x_A+x_B<2$ . Firm A uses personalized pricing and is the follower; B posts one uniform price first. The unique optimal leader price is

p_B=\frac{t(x_B-x_A)(2-x_A-x_B)}{2}.

The resulting gross profits are $t(x_B-x_A)(2+x_A+x_B)^2/16$ for A and $t(x_B-x_A)(2-x_A-x_B)^2/8$ for B. The statement links the Section 6 formulas to the pricing primitives rather than defining profits by those formulas.

Formalization Note The strict location and sum bounds select the interior demand regime. The leader's optimality ranges over all real prices; an indifferent consumer buys from the targeting follower.

Preamble

import Mathlib
import Definitions.Def_PPDifferentiation_ShortRun_Setting

Formal statement

namespace PPDifferentiation.ShortRun

theorem asymmetric_profits (t xA xB : ℝ) (ht : 0 < t)
    (hord : xA < xB) (hlo : -2 < xA + xB) (hhi : xA + xB < 2) :
    let p := t * (2 - xA - xB) * (xB - xA) / 2
    PPDifferentiation.Costless.IsLeaderOpt t xB xA p ∧
    (∀ q : ℝ, PPDifferentiation.Costless.IsLeaderOpt t xB xA q → q = p) ∧
    PPDifferentiation.Costless.followProf t xB xA p = t * (xB - xA) * (2 + xA + xB)^2 / 16 ∧
    PPDifferentiation.Costless.leadProf t xB xA p = t * (xB - xA) * (2 - xA - xB)^2 / 8 := by sorry

end PPDifferentiation.ShortRun

Source

Li, Wang, Nault, Is Personalized Pricing Profitable When Firms Can Differentiate?, working paper, SSRN abstract 3881900 (version of August 3, 2021), §6, p. 24, “Only one firm implements PP”; Appendix A, p. 33, proof of Lemma 1

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