The infinite graphon sampler as an exchangeable law

There are two constructions of an infinite random graph associated to a graphon. The explicit joint sampler infiniteSampleLaw draws all vertex positions and edge coins on one probability space. Independently, the finite sampling laws form sampleExchangeableLaw, whose consistent marginals have a unique extension to an infinite exchangeable law through exchangeableGraphLawEquivInfinite.

This file identifies those constructions. They have the same restriction to every finite window, so extensionality of measures on infinite graphs shows that their laws agree. In particular, the explicit joint sampling law is invariant under every permutation of its vertex labels. It then descends this law to graphon space and proves that the descended sampler is measurable.

Main definitions

• TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace — the joint sampling law of an infinite random graph, as a function of the graphon class.

Main results

• TauCeti.DenseGraphLimits.infiniteSampleLaw_eq_extension — the explicit joint sampler is the infinite extension of its finite sampling laws;
• TauCeti.DenseGraphLimits.infiniteSampleLaw_map_comap — the explicit joint sampler is invariant under relabelling by every permutation of ℕ;
• TauCeti.DenseGraphLimits.infiniteSampleLaw_eq_of_cutDist_eq_zero — graphons at cut distance zero, on arbitrary carriers, have the same joint sampling law;
• TauCeti.DenseGraphLimits.measurable_infiniteSampleLawOnSpace — the joint sampling law depends measurably on the graphon class.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteSampler.lean. The identification here follows map_sampleInfinite and map_sampleInfinite_eq_infiniteSampleLaw_mk, adapted to the finite-window extensionality API for Tau Ceti's laws on SimpleGraph ℕ.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_eq_extension {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : infiniteSampleLaw W = (exchangeableGraphLawEquivInfinite (sampleExchangeableLaw W)).law

The explicit infinite sampler realizes the abstract extension. The joint sampling law of a graphon equals the unique infinite exchangeable law whose finite marginals are the graphon's finite sampling laws.

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_map_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) (infiniteSampleLaw W) = infiniteSampleLaw W

The infinite joint sampling law of a graphon is invariant under relabelling along every permutation of ℕ.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_eq_of_cutDist_eq_zero {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (h : cutDist U W = 0) : infiniteSampleLaw U = infiniteSampleLaw W

Joint sampling laws are invariant at cut distance zero. Two graphons, on arbitrary probability carriers, at cut distance zero have the same law of the infinite random graph: a law on infinite graphs is determined by its finite windows, and those are the finite sampling laws.

noncomputable def TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : GraphonSpace Ω μ → MeasureTheory.Measure (SimpleGraph ℕ)

The law of the infinite random graph as a function of the graphon class. It is well defined because joint sampling laws are invariant at cut distance zero.

Equations

• TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace = SeparationQuotient.lift TauCeti.DenseGraphLimits.infiniteSampleLaw ⋯

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : infiniteSampleLawOnSpace (SeparationQuotient.mk W) = infiniteSampleLaw W

On a representative, the descended joint sampling law is the joint sampling law.

instance TauCeti.DenseGraphLimits.isProbabilityMeasure_infiniteSampleLawOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) : MeasureTheory.IsProbabilityMeasure (infiniteSampleLawOnSpace x)

An infinite sample from a graphon class has a probability law.

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace_map_restrictFin {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) (n : ℕ) : MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin n) (infiniteSampleLawOnSpace x) = sampleGraphOnSpace n x

The finite windows of the descended joint sampling law are the descended finite sampling laws.

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace_map_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) (infiniteSampleLawOnSpace x) = infiniteSampleLawOnSpace x

The descended joint sampling law is invariant under relabelling along every permutation of ℕ.

theorem TauCeti.DenseGraphLimits.measurable_infiniteSampleLawOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Measurable infiniteSampleLawOnSpace

The joint sampling law depends measurably on the graphon class. The window cylinders generate the σ-algebra on infinite graphs, and the mass of a cylinder is the mass of a finite graph under the descended finite sampling law.