Table 1 — stage-1 implementation payoffs

Proved

PPDifferentiation.ShortRun.table_1

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

hotellingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1payoff-matrixpersonalized-pricing

Let $t>0$ and $F\ge0$ . The firms choose PP or uniform pricing (U) before positioning. For every optimal uniform-leader price in each asymmetric continuation, the net stage-1 payoff matrix, with A's payoff first, is

\begin{array}{c|cc} & B:PP & B:U\\\hline A:PP &(t/8-F,t/8-F)&(t/4-F,t/2)\\ A:U &(t/2,t/4-F)&(3t/4,3t/4) \end{array}.

Every entry evaluates a gross pricing-stage payoff at the corresponding positioning outcome; $F$ is subtracted only from a firm that implements PP. This matrix supplies the comparisons in Proposition 5.

Formalization Note The theorem is conditional on the two leader prices being optimal; Proposition 5 also asserts those optima exist. The asymmetric continuation with B implementing PP is obtained by reflection of the source's A-implements-PP case.

Preamble

import Mathlib
import Definitions.Def_PPDifferentiation_ShortRun_Setting

Formal statement

namespace PPDifferentiation.ShortRun

theorem table_1 (t F : ℝ) (ht : 0 < t) (hF : 0 ≤ F) :
    ∀ p₀ p₁ : ℝ, PPDifferentiation.Costless.IsLeaderOpt t (1/2) (-1/2) p₀ →
      PPDifferentiation.Costless.IsLeaderOpt t (1/2) (3/2) p₁ →
      stage1A t F p₀ p₁ .PP .PP = t/8 - F ∧
      stage1B t F p₀ p₁ .PP .PP = t/8 - F ∧
      stage1A t F p₀ p₁ .PP .U = t/4 - F ∧
      stage1B t F p₀ p₁ .PP .U = t/2 ∧
      stage1A t F p₀ p₁ .U .PP = t/2 ∧
      stage1B t F p₀ p₁ .U .PP = t/4 - F ∧
      stage1A t F p₀ p₁ .U .U = 3*t/4 ∧
      stage1B t F p₀ p₁ .U .U = 3*t/4 := 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, Table 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