Weak convergence of graphon mixtures (issue #33, analytic layer)

The compactness infrastructure for the Diaconis–Janson representation theorem (steps 3–4 of the #33 plan; the integral bridge mixturePMF_apply_toReal and the weak continuity continuous_mixturePMF_apply_toReal live with the mixture definitions in Graphon/ExchangeableGraphLaw.lean):

• GraphonSpace.exists_subseq_tendsto — Prokhorov extraction: every sequence of mixing measures on the compact metrizable graphon space has a weakly convergent subsequence (Mathlib's CompactSpace (ProbabilityMeasure _) + metrizability);
• GraphonSpace.graphClass / GraphonSpace.empiricalMixing — the graphon class of a finite simple graph, and the empirical mixing measure of an exchangeable law at size n (the pushforward of L.law n under graphClass).

The remaining #33 content is the collision-bound marginal identification (step 5) and Stone–Weierstrass uniqueness (step 6).

theorem GraphonSpace.exists_subseq_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (Ps : ℕ → MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : ∃ (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (Ps ∘ φ) Filter.atTop (nhds P)

Prokhorov extraction: every sequence of mixing measures on the compact metrizable graphon space has a weakly convergent subsequence.

noncomputable def GraphonSpace.graphClass {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) : GraphonSpace α μ

The graphon class of a finite simple graph (its embedded step graphon, in the graphon space).

Equations

• GraphonSpace.graphClass G = GraphonSpace.mk (Graphon.ofSimpleGraphOn G)

noncomputable def GraphonSpace.empiricalMixing {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) (n : ℕ) [NeZero n] : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)

The empirical mixing measure of an exchangeable graph law at size n: sample Gₙ ∼ L.law n and take its graphon class. Step 3 of the #33 plan; Prokhorov extraction applies to the sequence fun n => empiricalMixing L (n + 1) — downstream statements use the successor form so the NeZero hypothesis discharges definitionally instead of recurring as bookkeeping.

Equations

• GraphonSpace.empiricalMixing L n = ⟨MeasureTheory.Measure.map GraphonSpace.graphClass (L.law n).toMeasure, ⋯⟩

@[simp]

theorem GraphonSpace.empiricalMixing_coe {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) (n : ℕ) [NeZero n] : ↑(empiricalMixing L n) = MeasureTheory.Measure.map graphClass (L.law n).toMeasure