Exchangeable laws on infinite graphs are integrals of joint sampling laws

A probability measure P on graphon space describes a two-stage infinite random graph: draw a graphon class from P, then run the joint sampler of that class on all of ℕ at once. This file identifies the two-stage law with the Giry-monad bind, so that the correspondence between mixing measures and exchangeable laws on infinite graphs reads as a genuine mixture on SimpleGraph ℕ.

With the mixture identity in hand, every exchangeable law on infinite graphs is the integral of joint sampling laws against one mixing measure on graphon space, and that mixing measure is unique. This is the integral form of the Diaconis–Janson correspondence; its finite-window form is mixtureExchangeableLaw.

A random graphon, given as a family of graphons over a probability space of parameters whose class depends almost-everywhere measurably on the parameter, produces such a mixture directly: sample the parameter, then run the joint sampler of the graphon it selects. The mixing measure of that law is the law of the class of the random graphon, carried into the unit-interval graphon space by toGraphonSpaceI; for graphons on the unit interval it is the law of the class itself. A jointly measurable family of graphons has a measurable class (measurable_graphonSpace_mk).

Main results

• TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_mixtureExchangeableLaw_law — the extension of a graphon mixture over an arbitrary probability carrier is the integral of the joint sampling laws;
• TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_law — the law attached to a mixing measure is the integral of the joint sampling laws against it;
• TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace — every exchangeable law on infinite graphs is such an integral, for exactly one mixing measure;
• TauCeti.DenseGraphLimits.bind_map_graphonSpace_mk_infiniteSampleLawOnSpace — mixing over the class of a random graphon is mixing over its representatives;
• TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_symm_eq_map — the mixing measure of a mixture of joint sampling laws over a random graphon is the law of the class of that random graphon in the unit-interval graphon space.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Theorem 5.3.

@[simp]

theorem TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_mixtureExchangeableLaw_law {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) : (exchangeableGraphLawEquivInfinite (mixtureExchangeableLaw P)).law = (↑P).bind infiniteSampleLawOnSpace

A graphon mixture is an integral of joint sampling laws. Extending the finite graphon mixture over an arbitrary probability carrier gives the bind of its mixing measure against the descended joint sampling law.

theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_law (P : MeasureTheory.ProbabilityMeasure GraphonSpaceI) : (graphonMixtureLawEquiv P).law = (↑P).bind infiniteSampleLawOnSpace

A graphon mixture is an integral of joint sampling laws. The exchangeable law on infinite graphs attached to a mixing measure P on graphon space is the bind of P against the descended joint sampling law: draw a graphon class from P, then run the infinite sampler.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace (L : InfiniteExchangeableGraphLaw) : ∃! P : MeasureTheory.ProbabilityMeasure GraphonSpaceI, (↑P).bind infiniteSampleLawOnSpace = L.law

Every exchangeable law on infinite graphs is a graphon mixture, for exactly one mixing measure. The integral form of the Diaconis–Janson correspondence: the law is the bind of a unique probability measure on graphon space against the joint sampling laws.

theorem TauCeti.DenseGraphLimits.bind_map_graphonSpace_mk_infiniteSampleLawOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Type u_2} [MeasurableSpace T] (ν : MeasureTheory.Measure T) {W : T → Graphon Ω μ} (hW : AEMeasurable (fun (t : T) => SeparationQuotient.mk (W t)) ν) : (MeasureTheory.Measure.map (fun (t : T) => SeparationQuotient.mk (W t)) ν).bind infiniteSampleLawOnSpace = ν.bind fun (t : T) => infiniteSampleLaw (W t)

Mixing over a random graphon. For a measure ν on parameters and a family of graphons W whose class is ν-almost-everywhere measurable in the parameter, mixing the descended joint sampling laws against the law of the class of W t is mixing the joint sampling laws of the graphons W t against ν.

theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_symm_eq_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Type u_2} [MeasurableSpace T] (L : InfiniteExchangeableGraphLaw) (ν : MeasureTheory.ProbabilityMeasure T) {W : T → Graphon Ω μ} (hW : AEMeasurable (fun (t : T) => SeparationQuotient.mk (W t)) ↑ν) (hL : L.law = (↑ν).bind fun (t : T) => infiniteSampleLaw (W t)) : graphonMixtureLawEquiv.symm L = ν.map fun (t : T) => toGraphonSpaceI (SeparationQuotient.mk (W t))

The mixing measure of a random graphon. If an exchangeable law on infinite graphs is the mixture, against a probability measure ν, of the joint sampling laws of a family W of graphons whose class is ν-almost-everywhere measurable in the parameter, then the mixing measure the Diaconis–Janson correspondence assigns to it is the law under ν of the class of W t in the unit-interval graphon space. For graphons on the unit interval, toGraphonSpaceI_eq_self removes the embedding.