Prove2Me

Theorem 3.20 — stability of Nash equilibria under graphon changes

Proved
GraphonGames.Stability.theorem_3_20_stability

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

graphon-gamenash-equilibriump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1stability

Assume Assumptions 1, 4, and 5. Let ww be a graphon with operator WW satisfying cz∥W∥<1\sqrt{c_z}\|W\|<1 and condition (17), and let α\alpha be its Nash equilibrium. Let w′w' be any graphon with operator W′W' satisfying cz∥W′∥<1\sqrt{c_z}\|W'\|<1, and let α′\alpha' be any Nash equilibrium for w′w'. Then

∥α−α′∥L2(I)≤κ∥W−W′∥,κ=c0ℓJ(1−cz∥W∥)(1−cz∥W∥)[ℓc(1−cz∥W∥)−ℓJcα∥W∥].\|\alpha-\alpha'\|_{L^2(I)}\leq\kappa\|W-W'\|,\qquad \kappa=\frac{c_0\ell_J(1-\sqrt{c_z}\|W\|)} {(1-\sqrt{c_z}\|W\|) [\ell_c(1-\sqrt{c_z}\|W\|)-\ell_J\sqrt{c_\alpha}\|W\|]}.

This quantifies how much an equilibrium profile can move when the graphon changes. The coefficient uses the original graphon's operator norm and the paper's uncancelled expression.

Formalization Note The equilibrium predicate uses the equivalent third condition of Proposition 3.6 and includes an aggregate for each graphon. The first equilibrium is given as a witness; Proposition 3.17 provides its existence and uniqueness. No condition (17) is imposed on w′w'. The norm of W−W′W-W' is the operator norm of w−w′w-w', and the inequality is in extended nonnegative reals.

Preamble
import Mathlib
import Definitions.Def_GraphonGames_Stability_Setting

open MeasureTheory
open scoped ENNReal
Formal statement
namespace GraphonGames.Stability

theorem theorem_3_20_stability
    (b : ℝ → ℝ → ℝ) (f : ℝ → ℝ → ℝ → ℝ)
    (μ0 : Measure ℝ) (cα cz ℓc ℓJ c0 : ℝ)
    (h1 : GraphonGames.Existence.Asm1 b μ0 cα cz)
    (h4 : GraphonGames.Existence.Asm4 (GraphonGames.Existence.cost b f μ0) ℓc ℓJ)
    (h5 : GraphonGames.Existence.Asm5 b c0)
    (w w' : I → I → ℝ) (hw : IsGraphon w) (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)
    (hW' : Real.sqrt cz * (opNorm w').toReal < 1)
    (α α' : I → ℝ)
    (hα : IsNash w b f μ0 α) (hα' : IsNash w' b f μ0 α') :
    eLpNorm (α - α') 2 volume ≤
      ENNReal.ofReal
        (c0 * ℓJ * (1 - Real.sqrt cz * (opNorm w).toReal) /
          ((1 - Real.sqrt cz * (opNorm w).toReal) *
            (ℓc * (1 - Real.sqrt cz * (opNorm w).toReal) -
              ℓJ * Real.sqrt cα * (opNorm w).toReal))) *
        opNorm (w - w') := by sorry

end GraphonGames.Stability
Source
Carmona, Cooney, Graves & Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1, p. 17, Theorem 3.20
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