(4) — asymmetric subgame gross profits

Proved

PPDifferentiation.ShortRun.asymmetric_equilibrium_profits

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

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

Let $t>0$ . With the targeting firm A at $-1/2$ and the uniform-price leader B at $1/2$ , an optimal leader price exists, and every optimal leader price gives gross subgame profits

\pi_A^{AS}=\frac{t}{4},\qquad\pi_B^{AS}=\frac{t}{2}.

These are gross profits because the implementation cost was already sunk before positioning. They supply the asymmetric cells of Table 1 after the PP firm's cost is subtracted.

Formalization Note The leader chooses from all real prices; the result explicitly rules out vacuity by asserting existence of an optimum. The covered-market reservation value cancels.

Preamble

import Mathlib
import Definitions.Def_PPDifferentiation_ShortRun_Setting

Formal statement

namespace PPDifferentiation.ShortRun

theorem asymmetric_equilibrium_profits (t : ℝ) (ht : 0 < t) :
    (∃ p : ℝ, PPDifferentiation.Costless.IsLeaderOpt t (1/2) (-1/2) p) ∧
    ∀ p : ℝ, PPDifferentiation.Costless.IsLeaderOpt t (1/2) (-1/2) p →
      PPDifferentiation.Costless.followProf t (1/2) (-1/2) p = t/4 ∧
      PPDifferentiation.Costless.leadProf t (1/2) (-1/2) p = t/2 := 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. 25, display (4)

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