Proposition 3.17 — existence and uniqueness under condition (17)

Proved

GraphonGames.Stability.proposition_3_17_unique_equilibrium

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

contractiongraphon-gamenash-equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Assume Assumptions 1 and 4. Let $w$ be a graphon with operator $W$ such that $\sqrt{c_z}\|W\|<1$ and

\frac{\ell_J}{\ell_c}\, \frac{\sqrt{c_\alpha}\|W\|}{1-\sqrt{c_z}\|W\|}<1.

Then the graphon game has a Nash equilibrium, and every Nash equilibrium is equal to it almost everywhere.

This gives the unique equilibrium named in the stability theorem.

Formalization Note Equilibrium uses the pointwise minimization condition of Proposition 3.6 and carries an aggregate satisfying (6). Uniqueness is of $L^2$ classes; no boundedness Assumption 5 is imposed.

Preamble

import Mathlib
import Definitions.Def_GraphonGames_Stability_Setting

open MeasureTheory

Formal statement

namespace GraphonGames.Stability

theorem proposition_3_17_unique_equilibrium
    (b : ℝ → ℝ → ℝ) (f : ℝ → ℝ → ℝ → ℝ)
    (μ0 : Measure ℝ) (cα cz ℓc ℓJ : ℝ)
    (h1 : GraphonGames.Existence.Asm1 b μ0 cα cz)
    (h4 : GraphonGames.Existence.Asm4 (GraphonGames.Existence.cost b f μ0) ℓc ℓJ)
    (w : I → I → ℝ) (hw : IsGraphon w)
    (hW : Real.sqrt cz * (opNorm w).toReal < 1)
    (h17 : ℓJ / ℓc *
      (Real.sqrt cα * (opNorm w).toReal /
        (1 - Real.sqrt cz * (opNorm w).toReal)) < 1) :
    ∃ α, IsNash w b f μ0 α ∧
      ∀ α', IsNash w b f μ0 α' → α' =ᵐ[volume] α := by sorry

end GraphonGames.Stability

Source

Carmona, Cooney, Graves & Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1, p. 15, Proposition 3.17 and (17)

Human review

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

View graph