Uniform mixtures of dissociated exchangeable graph laws

Every exchangeable law on infinite graphs is a measurable mixture of dissociated exchangeable graph laws, with one uniform variable on the unit interval as the mixing variable (InfiniteExchangeableGraphLaw.exists_dissociated_kernel): the components are exchangeable probability measures on the graphs on ℕ, almost all of them dissociated, and their mixture against the uniform law is the original law. This is the ergodic decomposition of an exchangeable graph law, with the extreme laws (mem_extremePoints_iff_isDissociated) as components; by InfiniteExchangeableGraphLaw.ae_eq_of_comp_eq a dissociated law is its own only decomposition. Representing the components by graphons is a separate step.

The graph decomposition is the array decomposition of the adjacency array (JointlyExchangeable.exists_dissociated_kernel) viewed on graphs: its components are the decoded components of the array decomposition, and the mixing variable is the same.

MeasureTheory.Measure.IsDissociatedGraphLaw packages the exchangeable probability measures on graphs whose finite law is dissociated, so that a component of the decomposition is described by one predicate.

Main results

• MeasureTheory.Measure.IsDissociatedGraphLaw — dissociated exchangeable probability measures on graphs, with isDissociatedGraphLaw_iff and its extreme-point form isDissociatedGraphLaw_iff_mem_extremePoints.
• TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.exists_dissociated_kernel — every exchangeable graph law is a uniform mixture of dissociated exchangeable graph laws.

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.

def MeasureTheory.Measure.IsDissociatedGraphLaw (μ : Measure (SimpleGraph ℕ)) : Prop

A dissociated exchangeable graph law: an exchangeable probability measure on the graphs on ℕ whose finite law is dissociated.

Equations

• μ.IsDissociatedGraphLaw = ∃ (L : TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw), L.law = μ ∧ (TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite.symm L).IsDissociated

theorem TauCeti.DenseGraphLimits.isDissociatedGraphLaw_iff {μ : MeasureTheory.Measure (SimpleGraph ℕ)} : μ.IsDissociatedGraphLaw ↔ ∃ (hp : MeasureTheory.IsProbabilityMeasure μ) (hex : ∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) μ = μ), (exchangeableGraphLawEquivInfinite.symm { law := μ, prob := hp, exchangeable := hex }).IsDissociated

A measure is a dissociated exchangeable graph law exactly when it is an exchangeable probability measure whose finite law is dissociated.

theorem TauCeti.DenseGraphLimits.isDissociatedGraphLaw_iff_mem_extremePoints {μ : MeasureTheory.Measure (SimpleGraph ℕ)} : μ.IsDissociatedGraphLaw ↔ μ ∈ Set.extremePoints ENNReal exchangeableGraphProbabilityMeasures

A dissociated exchangeable graph law is an extreme exchangeable graph measure, and conversely.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.exists_dissociated_kernel (L : InfiniteExchangeableGraphLaw) : ∃ (κ : ProbabilityTheory.Kernel (↑unitInterval) (SimpleGraph ℕ)), ProbabilityTheory.IsMarkovKernel κ ∧ (∀ᵐ (u : ↑unitInterval), (κ u).IsDissociatedGraphLaw) ∧ MeasureTheory.volume.bind ⇑κ = L.law

Every exchangeable graph law is a uniform mixture of dissociated exchangeable graph laws. The components are dissociated exchangeable graph laws for almost every value of one uniform variable on the unit interval, and their mixture is the original law.