Proposition 3.1 — existence and uniqueness of the aggregate

Proved

GraphonGames.Stability.proposition_3_1_aggregate_exists_unique

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

aggregatefixed-pointgraphon-gamep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $w$ be a real, symmetric, square-integrable graphon with integral operator $W$ . Suppose the state map $b$ and centered noise law satisfy Assumption 1 with constants $c_\alpha,c_z\geq0$ , and $\sqrt{c_z}\|W\|<1$ . For every $L^2$ strategy profile $\alpha$ , there is an $L^2$ aggregate $z$ satisfying

z(x)=\int_I w(x,y)b(\alpha(y),z(y))\,dy\quad\text{for almost every }x\in I,

and every other such aggregate equals $z$ almost everywhere.

This defines the aggregate operator used throughout the graphon game.

Formalization Note Uniqueness is of $L^2$ equivalence classes, so it is stated as almost-everywhere equality. The centered noise law is part of the standing Assumption 1 representation.

Preamble

import Mathlib
import Definitions.Def_GraphonGames_Stability_Setting

open MeasureTheory

Formal statement

namespace GraphonGames.Stability

theorem proposition_3_1_aggregate_exists_unique
    (b : ℝ → ℝ → ℝ) (μ0 : Measure ℝ) (cα cz : ℝ)
    (h1 : GraphonGames.Existence.Asm1 b μ0 cα cz)
    (w : I → I → ℝ) (hw : IsGraphon w)
    (hW : Real.sqrt cz * (opNorm w).toReal < 1)
    (α : I → ℝ) (hα : MemLp α 2 volume) :
    ∃ z, IsAggregate w b α z ∧
      ∀ z', IsAggregate w b α z' → z' =ᵐ[volume] z := by sorry

end GraphonGames.Stability

Source

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

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