The Diaconis–Janson graphon-mixture representation theorem (issue #33)

Assembly of the two halves proved in Graphon/MixtureUniqueness.lean and Graphon/MixtureExistence.lean:

• GraphonSpace.graphon_mixture_representation — the representation theorem: every exchangeable graph law is the mixture law of a unique probability measure on the graphon space;
• GraphonSpace.mixtureExchangeableLawEquiv — the packaged bijection ProbabilityMeasure (GraphonSpace α μ) ≃ Graphon.ExchangeableGraphLaw;
• GraphonSpace.empiricalMixing_tendsto_representingMeasure — empirical convergence: the whole sequence of empirical mixing measures converges weakly to the representing measure (subsequential limits are unique by the representation theorem, and a unique cluster point in a compact metrizable space gives convergence).

theorem GraphonSpace.graphon_mixture_representation {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) : ∃! P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ), mixtureExchangeableLaw P = L

The graphon-mixture representation theorem (Diaconis–Janson): every exchangeable graph law is the mixture law of a unique probability measure on the graphon space — existence by exists_mixtureExchangeableLaw_eq, uniqueness by mixtureExchangeableLaw_injective.

noncomputable def GraphonSpace.mixtureExchangeableLawEquiv {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ) ≃ Graphon.ExchangeableGraphLaw

The graphon-mixture representation, packaged as a bijection between mixing measures on the graphon space and exchangeable graph laws.

Equations

• GraphonSpace.mixtureExchangeableLawEquiv = Equiv.ofBijective GraphonSpace.mixtureExchangeableLaw ⋯

@[simp]

theorem GraphonSpace.mixtureExchangeableLawEquiv_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : mixtureExchangeableLawEquiv P = mixtureExchangeableLaw P

@[simp]

theorem GraphonSpace.mixtureExchangeableLawEquiv_symm_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) : mixtureExchangeableLaw (mixtureExchangeableLawEquiv.symm L) = L

theorem GraphonSpace.empiricalMixing_tendsto_representingMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) : Filter.Tendsto (fun (n : ℕ) => empiricalMixing L (n + 1)) Filter.atTop (nhds (mixtureExchangeableLawEquiv.symm L))

Empirical convergence to the representing measure: the whole sequence of empirical mixing measures of an exchangeable law converges weakly to the unique representing measure — not merely a subsequence. Every subsequence has a Prokhorov sub-subsequential limit; the collision estimate identifies each such limit's mixture law with L; uniqueness forces every limit to be the representing measure; and a unique cluster point in a compact metrizable space gives convergence.