Dissociated exchangeable graph laws as dissociated relational laws

An exchangeable graph law is dissociated (ExchangeableGraphLaw.IsDissociated) when the random graphs it induces on disjoint label windows are independent; an exchangeable relational law is dissociated (TauCeti.Probability.ExchangeableRelationalLaw.IsDissociated) when the random configurations it induces on disjoint vertex windows are. Encoding simple graphs as configurations of the language of graphs commutes with restriction to a window, and the encoding is a measurable embedding, so it neither creates nor destroys independence: a graph law is dissociated exactly when its relational law is.

Combined with the extremality of graphon sampling laws among exchangeable graph laws (exists_graphon_of_isDissociated), this identifies the dissociated exchangeable relational laws of the language of graphs concentrated on simple graphs: they are exactly the relational laws of graphon sampling laws.

Main results

• TauCeti.DenseGraphLimits.ExchangeableGraphLaw.isDissociated_toRelationalLaw_iff — a graph law is dissociated exactly when its relational law is;
• TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw — an exchangeable relational law of the language of graphs concentrated on simple graphs is dissociated exactly when it is the relational law of a graphon sampling law.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.

@[simp]

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.isDissociated_toRelationalLaw_iff (L : ExchangeableGraphLaw) : L.toRelationalLaw.IsDissociated ↔ L.IsDissociated

A graph law is dissociated exactly when its relational law is: encoding graphs as configurations of the language of graphs neither creates nor destroys independence of disjoint windows.

theorem TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ] {ν : Probability.ExchangeableRelationalLaw FirstOrder.Language.graph} (hν : ∀ (n : ℕ), ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂ν.law n, c.IsSimpleGraph) : ν.IsDissociated ↔ ∃ (W : Graphon Ω μ), ν = (sampleExchangeableLaw W).toRelationalLaw

Dissociated relational laws of graphs are graphon sampling laws. An exchangeable relational law of the language of graphs whose marginals are concentrated on simple graphs is dissociated exactly when it is the relational law of the sampling law of a graphon, which may be taken on any atomless standard Borel carrier (Ω, μ), such as the unit interval.