Exchangeable graph laws correspond to mixing measures on graphon space

The mixture map from probability measures on the graphon space over the unit interval to exchangeable graph laws is injective (mixtureExchangeableLaw_injective): a mixture law determines its mixing measure. Together with existence (exists_mixtureExchangeableLaw_eq) this makes the mixture map a bijection, packaged as mixtureExchangeableLawEquiv. This is the Diaconis–Janson correspondence at the level of the finite marginals. Uniqueness holds on the graphon quotient GraphonSpaceI, not among graphon representatives.

Main definitions

• TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv — the mixture map, as an equivalence between probability measures on GraphonSpaceI and exchangeable graph laws.

Main results

• TauCeti.DenseGraphLimits.mixtureExchangeableLaw_injective — a mixture law determines its mixing measure.
• TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv_apply — the equivalence is the mixture map.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33–61, Section 5.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 11.3.

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLaw_injective : Function.Injective mixtureExchangeableLaw

Uniqueness of the mixing measure. Two probability measures on GraphonSpaceI with the same mixture law are equal.

noncomputable def TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv : MeasureTheory.ProbabilityMeasure GraphonSpaceI ≃ ExchangeableGraphLaw

The Diaconis–Janson correspondence. The mixture map is an equivalence between probability measures on GraphonSpaceI and exchangeable graph laws.

Equations

• TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv = Equiv.ofBijective TauCeti.DenseGraphLimits.mixtureExchangeableLaw TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv._proof_1✝

@[simp]

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLawEquiv_apply (P : MeasureTheory.ProbabilityMeasure GraphonSpaceI) : mixtureExchangeableLawEquiv P = mixtureExchangeableLaw P

The forward map of mixtureExchangeableLawEquiv is the mixture map.