The infinite exchangeable graph law: existence and uniqueness (brick A2)

Every exchangeable graph law extends uniquely to a probability law on the infinite graph space — a specialized Kolmogorov extension proved from compactness, with no general projective-limit machinery:

• InfiniteGraph.restrictFin_padFin_of_le — padding then restricting to a lower level is restriction along Fin.castLE;
• Graphon.ExchangeableGraphLaw.paddedLaw — the level-n law pushed forward through padFin, a probability measure on InfiniteGraph; its level-k restriction is exactly L.law k for every k ≤ n (paddedLaw_map_restrictFin, by consistency);
• Graphon.ExchangeableGraphLaw.infiniteLaw — the infinite law: a Prokhorov subsequential limit of the padded laws. Weak convergence against the continuous finite restrictions identifies every marginal (infiniteLaw_map_restrictFin), and finite-restriction measure extensionality gives uniqueness (unique_of_map_restrictFin / eq_infiniteLaw_of_map_restrictFin).

Brick A3 (exchangeability of infiniteLaw under every permutation of ℕ, and the packaged equivalence with ExchangeableGraphLaw) builds on this.

theorem InfiniteGraph.restrictFin_padFin_of_le {k n : ℕ} (h : k ≤ n) (H : SimpleGraph (Fin n)) : restrictFin k (padFin H) = SimpleGraph.comap (⇑(Fin.castLEEmb h)) H

Padding to level n and restricting to a lower level k is restriction along Fin.castLE.

noncomputable def Graphon.ExchangeableGraphLaw.paddedLaw (L : ExchangeableGraphLaw) (n : ℕ) : MeasureTheory.ProbabilityMeasure InfiniteGraph

The padded law at level n: the n-vertex law, pushed forward to the infinite graph space through padFin.

Equations

• L.paddedLaw n = ⟨MeasureTheory.Measure.map InfiniteGraph.padFin (L.law n).toMeasure, ⋯⟩

@[simp]

theorem Graphon.ExchangeableGraphLaw.paddedLaw_coe (L : ExchangeableGraphLaw) (n : ℕ) : ↑(L.paddedLaw n) = MeasureTheory.Measure.map InfiniteGraph.padFin (L.law n).toMeasure

theorem Graphon.ExchangeableGraphLaw.paddedLaw_map_restrictFin (L : ExchangeableGraphLaw) {k n : ℕ} (h : k ≤ n) : MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑(L.paddedLaw n) = (L.law k).toMeasure

The level-k restriction of the padded level-n law is exactly the k-vertex law, for every k ≤ n (consistency along Fin.castLE).

theorem InfiniteGraph.exists_subseq_tendsto (Ps : ℕ → MeasureTheory.ProbabilityMeasure InfiniteGraph) : ∃ (P : MeasureTheory.ProbabilityMeasure InfiniteGraph) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (Ps ∘ φ) Filter.atTop (nhds P)

Prokhorov extraction on the infinite graph space: every sequence of probability measures has a weakly convergent subsequence.

theorem Graphon.ExchangeableGraphLaw.unique_of_map_restrictFin {L : ExchangeableGraphLaw} {P Q : MeasureTheory.ProbabilityMeasure InfiniteGraph} (hP : ∀ (k : ℕ), MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑P = (L.law k).toMeasure) (hQ : ∀ (k : ℕ), MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑Q = (L.law k).toMeasure) : P = Q

The marginal property has at most one solution (finite-restriction measure extensionality).

theorem Graphon.ExchangeableGraphLaw.exists_map_restrictFin_eq (L : ExchangeableGraphLaw) : ∃ (P : MeasureTheory.ProbabilityMeasure InfiniteGraph), ∀ (k : ℕ), MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑P = (L.law k).toMeasure

Existence of the infinite law: a Prokhorov subsequential limit of the padded laws has every finite restriction equal to the corresponding marginal.

noncomputable def Graphon.ExchangeableGraphLaw.infiniteLaw (L : ExchangeableGraphLaw) : MeasureTheory.ProbabilityMeasure InfiniteGraph

The infinite exchangeable graph law (specialized Kolmogorov extension via compactness): the unique probability law on the infinite graph space whose finite restrictions are the given marginals.

Equations

• L.infiniteLaw = ⋯.choose

theorem Graphon.ExchangeableGraphLaw.infiniteLaw_map_restrictFin (L : ExchangeableGraphLaw) (k : ℕ) : MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑L.infiniteLaw = (L.law k).toMeasure

The marginal identification: each finite restriction of the infinite law is the corresponding finite marginal.

theorem Graphon.ExchangeableGraphLaw.eq_infiniteLaw_of_map_restrictFin {L : ExchangeableGraphLaw} {P : MeasureTheory.ProbabilityMeasure InfiniteGraph} (hP : ∀ (k : ℕ), MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑P = (L.law k).toMeasure) : P = L.infiniteLaw

Uniqueness: any probability law with the correct finite restrictions is the infinite law.

theorem Graphon.ExchangeableGraphLaw.infiniteLaw_injective : Function.Injective infiniteLaw

The infinite law determines the exchangeable law (injectivity of the extension): two exchangeable laws with the same infinite law are equal.