Proof of Proposition 4, p. 50 — g(n; 3) − g(n; 2) = −ln 2 + 1/(1 − n/2) − 1/(1 − n) + γn

Proved

NetFeePlatform.Competition.gChar_three_sub_two

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

logit-demandmarket-dominancep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1platform-competition

For every $\gamma\in\mathbb R$ and every $0<n<1$ , the characterization functions for triopoly and duopoly differ by

g(n;3)-g(n;2)=-\ln2+\frac{1}{1-n/2}-\frac{1}{1-n}+\gamma n.

At a zero of $g(\cdot;2)$ , i.e. a duopoly equilibrium whose smaller platform has share $n$ , the sign of this difference is the sign of $g(n;3)$ , which decides whether triopoly has an equilibrium with an even larger dominant platform.

Preamble

import Mathlib
import Definitions.Def_NetFeePlatform_Competition_Setting
import Definitions.Def_NetFeePlatform_Competition_GChar

Formal statement

namespace NetFeePlatform.Competition
theorem gChar_three_sub_two (γ n : ℝ) (hn0 : 0 < n) (hn1 : n < 1) :
    gChar γ 3 n - gChar γ 2 n = -Real.log 2 + 1 / (1 - n / 2) - 1 / (1 - n) + γ * n := by sorry
end NetFeePlatform.Competition

Source

Ekmekci, White & Wu, Platform Competition and Interoperability: The Net Fee Model, accepted working-paper version (December 12, 2024), pp. 49–50, Appendix E.2, proof of Proposition 4

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph