§6 — both-PP positioning equilibrium and gross profits

Proved

PPDifferentiation.ShortRun.both_pp_positions

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

hotellingnash-equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1personalized-pricing

For $t>0$ , when both firms have already implemented personalized pricing, the positioning subgame has an equilibrium at $x_A=1/4$ and $x_B=3/4$ . With the implementation costs already sunk, each firm's gross subgame profit is

\pi_A^{PP}=\pi_B^{PP}=\frac{t}{8}.

The equilibrium compares deviations to all real positions. These gross profits become the both-PP cell of the implementation game after subtracting $F$ from each firm.

Formalization Note The gross profit is the consumer-by-consumer Bertrand integral; the reservation value cancels under full coverage.

Preamble

import Mathlib
import Definitions.Def_PPDifferentiation_ShortRun_Setting

Formal statement

namespace PPDifferentiation.ShortRun

theorem both_pp_positions (t : ℝ) (ht : 0 < t) :
    PPDifferentiation.Costless.IsPosEqPP t (1/4) (3/4) ∧
    PPDifferentiation.Costless.profPP t (1/4) (3/4) = t/8 ∧
    PPDifferentiation.Costless.profPP t (3/4) (1/4) = t/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, pp. 23–24, “Both firms implement PP”

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