Lemma 3.19 — aggregate stability under a change of graphon

Proved

GraphonGames.Stability.lemma_3_19_aggregate_graphon_stability

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

aggregategraphon-gamep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1stability

Under Assumptions 1, 4, and 5, let $w,w'$ be graphons with operators $W,W'$ satisfying $\sqrt{c_z}\|W\|<1$ and $\sqrt{c_z}\|W'\|<1$ . For a fixed $L^2$ strategy profile $\alpha$ , let $Z\alpha$ and $Z'\alpha$ be its aggregates under $w$ and $w'$ . Then

\|Z\alpha-Z'\alpha\|_{L^2(I)}\leq \frac{c_0}{1-\sqrt{c_z}\|W\|}\|W-W'\|.

This isolates the effect of changing the interaction kernel while keeping actions fixed.

Formalization Note The right side uses the operator norm of the difference kernel. Assumption 4 is retained as printed, although this estimate does not use it in the paper's proof.

Preamble

import Mathlib
import Definitions.Def_GraphonGames_Stability_Setting

open MeasureTheory
open scoped ENNReal

Formal statement

namespace GraphonGames.Stability

theorem lemma_3_19_aggregate_graphon_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)
    (hW' : Real.sqrt cz * (opNorm w').toReal < 1)
    (α : I → ℝ) (hα : MemLp α 2 volume)
    (z z' : I → ℝ) (hz : IsAggregate w b α z)
    (hz' : IsAggregate w' b α z') :
    eLpNorm (z - z') 2 volume ≤
      ENNReal.ofReal
        (c0 / (1 - Real.sqrt cz * (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, Lemma 3.19

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