Prove2Me

Appendix A1, PDF p. 28 (printed p. 22) — e_p − e̲ = (t − μ)(2t − μ)/(2t) > 0

Proved
Multihoming.Thresholds.eLow_lt_eP

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

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

Let t>0t>0 and 0≤μ<t0\le\mu<t, with e‾=(t−μ)(2t+μ)/(2t)\underline e=(t-\mu)(2t+\mu)/(2t) the lower end of the partial-multihoming range (24) and ep=2(t−μ)e_p=2(t-\mu). Then

ep−e‾=(t−μ)(2t−μ)2t>0.e_p-\underline e=\frac{(t-\mu)(2t-\mu)}{2t}>0 .

So the price threshold lies strictly above the lower end of the partial-multihoming range.

Preamble
import Mathlib
import Definitions.Def_Multihoming_Thresholds_Model
Formal statement
namespace Multihoming.Thresholds

theorem eLow_lt_eP (t μ : ℝ) (ht : 0 < t) (hμ : 0 ≤ μ) (hμt : μ < t) :
    eP t μ - eLow t μ = (t - μ) * (2 * t - μ) / (2 * t) ∧ eLow t μ < eP t μ := 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_p − e̲ = …"
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