Dissociated exchangeable graph laws are sampling laws

A graphon mixture over an arbitrary probability carrier is dissociated exactly when its mixing measure is the Dirac mass at one graphon class (isDissociated_mixtureExchangeableLaw_iff). Hence a dissociated exchangeable graph law is the sampling law of a single graphon, which can be taken on any atomless standard Borel carrier, such as the unit interval (exists_graphon_of_isDissociated). Together with isDissociated_sampleExchangeableLaw this identifies the dissociated exchangeable graph laws with the sampling laws of graphons.

The route is through the homomorphism-density coordinates. Under any mixing measure of a dissociated law, every homomorphism density is almost surely equal to the corresponding upper mass (ae_homDensityOnSpace_eq_upperMass_of_isDissociated), so all homomorphism-density coordinates are almost surely constant at once; since they separate graphon classes, almost every class is the same one. The representing graphon is unique only up to cut distance zero.

Main results

• TauCeti.DenseGraphLimits.ae_homDensityOnSpace_eq_upperMass_of_isDissociated — under a mixing measure of a dissociated law, t(F, ·) is almost surely the upper mass of F.
• TauCeti.DenseGraphLimits.isDissociated_mixtureExchangeableLaw_iff — a graphon mixture is dissociated exactly when its mixing measure is a Dirac mass.
• TauCeti.DenseGraphLimits.exists_graphon_of_isDissociated — every dissociated exchangeable graph law is the sampling law of a graphon on every atomless standard Borel carrier.

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.ae_homDensityOnSpace_eq_upperMass_of_isDissociated {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) (h : (mixtureExchangeableLaw P).IsDissociated) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : ∀ᵐ (x : GraphonSpace Ω μ) ∂↑P, homDensityOnSpace F x = (mixtureExchangeableLaw P).upperMass F

Under a mixing measure of a dissociated exchangeable graph law, each homomorphism density is almost surely constant, equal to the upper mass of the pattern.

theorem TauCeti.DenseGraphLimits.isDissociated_mixtureExchangeableLaw_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) : (mixtureExchangeableLaw P).IsDissociated ↔ ∃ (W : Graphon Ω μ), P = MeasureTheory.diracProba (SeparationQuotient.mk W)

Dissociated mixtures are Dirac mixtures. A graphon mixture, over an arbitrary probability carrier, is dissociated exactly when its mixing measure is the Dirac mass at one graphon class.

theorem TauCeti.DenseGraphLimits.exists_graphon_of_isDissociated {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] (L : ExchangeableGraphLaw) (h : L.IsDissociated) : ∃ (W : Graphon Ω μ), L = sampleExchangeableLaw W

Dissociated laws are sampling laws. Every dissociated exchangeable graph law is the sampling law of a graphon on every atomless standard Borel carrier (Ω, μ), such as the unit interval.