Proof of Proposition 1, p. 10 — convergence from either side of the middle equilibrium

Proved

NetExtDominance.Introspective.converge_by_side

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

equilibrium-selectionmonotone-dynamicsnetwork-externalitiesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let the market have In/Out inverse demand and $p_{\min}\le p\le p_{\max}$ . Choose the out, middle, and in branch equilibria $q_{\mathrm{out}}$ , $q_{\mathrm{mid}}$ , and $q_{\mathrm{in}}$ . For any impulse $I_0\in[0,1]$ , the sequence $I_k=D(p,\cdot)^{\circ k}(I_0)$ satisfies

\begin{cases} I_k\to q_{\mathrm{in}},& I_0>q_{\mathrm{mid}},\\ I_k=I_0\text{ for every }k,& I_0=q_{\mathrm{mid}},\\ I_k\to q_{\mathrm{out}},& I_0<q_{\mathrm{mid}}. \end{cases}

This is the convergence claim in the first paragraph of the proof of Proposition 1.

Formalization Note At a threshold price, adjacent branch equilibria may coincide; the three implications still have their stated meanings.

Preamble

import Mathlib
import Definitions.Def_NetExtDominance_Introspective_Setting

Formal statement

namespace NetExtDominance.Introspective

/-- Proof of Proposition 1, first paragraph: the impulse's side of the middle
equilibrium determines the limit, and the middle point remains fixed. -/
theorem converge_by_side
    (M : Market) (QL QH : ℝ) (hIO : IsInOut M.P QL QH)
    (p : ℝ) (hp1 : pmin M.P QL ≤ p) (hp2 : p ≤ pmax M.P QH)
    (qo qm qi : ℝ) (ho : IsQout M.P QL p qo)
    (hm : IsQmid M.P QL QH p qm) (hi : IsQin M.P QH p qi)
    (I0 : ℝ) (hI0 : I0 ∈ Set.Icc (0 : ℝ) 1) :
    (qm < I0 → IsIntrospectiveEq M p I0 qi) ∧
      (I0 < qm → IsIntrospectiveEq M p I0 qo) ∧
      (I0 = qm → ∀ k, levelK M p I0 k = I0) := by sorry

end NetExtDominance.Introspective

Source

Akerlof, Holden & Rayo, Network Externalities and Market Dominance, author's accepted manuscript (WRAP 178238, dated September 16, 2022), p. 10, proof of Proposition 1, first paragraph; http://wrap.warwick.ac.uk/178238

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