Appendix A1, PDF pp. 27–28 (printed pp. 21–22) — e_π − e_p = 2(2t − μ)(t√(t² − μ²) − (t − μ)²)/(4t² − 3tμ + μ²)

Proved

Multihoming.Thresholds.ePi_sub_eP

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

hotellingnetwork-effectsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $t>0$ and $0\le\mu<t$ , with $e_p=2(t-\mu)$ the price threshold and $e_\pi$ the profit threshold of Appendix A1. Then

e_\pi-e_p=2(2t-\mu)\,\frac{t\sqrt{t^2-\mu^2}-(t-\mu)^2}{4t^2-3t\mu+\mu^2}.

This identity reduces the comparison $e_p<e_\pi$ to the sign of $t\sqrt{t^2-\mu^2}-(t-\mu)^2$ .

Preamble

import Mathlib
import Definitions.Def_Multihoming_Thresholds_Model

Formal statement

namespace Multihoming.Thresholds

theorem ePi_sub_eP (t μ : ℝ) (ht : 0 < t) (hμ : 0 ≤ μ) (hμt : μ < t) :
    ePi t μ - eP t μ =
      2 * (2 * t - μ) * (t * Real.sqrt (t ^ 2 - μ ^ 2) - (t - μ) ^ 2) /
        (4 * t ^ 2 - 3 * t * μ + μ ^ 2) := by sorry

end Multihoming.Thresholds

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 p. 28 (printed p. 22), Appendix A1, display "e_π − e_p = …" (introduced at the foot of PDF p. 27)

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