Appendix A1, PDF pp. 28–29 (printed pp. 22–23) — πᴹ(μ = 0) > πᴹ(μ = t)

Proved

Multihoming.Hump.profit_zero_gt_profit_t

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

comparative-staticshotellingnetwork-effectsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $t>0$ and $e>0$ , and let $\pi^M(\mu)=t(t-\mu)(e+\mu)^2/((t+\mu)(2t-\mu)^2)$ be the symmetric profit (26). Then

\pi^M(\mu=0)>\pi^M(\mu=t).

Maximized profits are thus larger without network effects than with network effects that are strong enough.

Formalization Note $\pi^M(t)=0$ and $\pi^M(0)=e^2/(4t)$ , so the statement needs $e>0$ , which is added: at $e=0$ both values are $0$ .

Preamble

import Mathlib
import Definitions.Def_Multihoming_Hump_Model

Formal statement

namespace Multihoming.Hump

/-- Appendix A1, PDF pp. 28–29: πᴹ(μ = 0) > πᴹ(μ = t) (for e > 0). -/
theorem profit_zero_gt_profit_t (t e : ℝ) (ht : 0 < t) (he0 : 0 < e) :
    piM t t e < piM t 0 e := by sorry

end Multihoming.Hump

Source

Foros, Kind & Stähler, Endogenous multihoming and network effects: PlayStation, Xbox, or both?, SNF Working Paper No. 16/21 (NHH Bergen, December 2021; Management Science DOI 10.1287/mnsc.2022.00613), PDF pp. 28–29 (printed pp. 22–23), Appendix A1, sentence "It is also immediately clear from (26) …"

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