Aldous–Hoover codings and graphon mixing measures

The graph law of a joint Boolean coding is a mixture of the sampling laws of its frozen coding graphons. Here we identify its unique mixing measure on graphon space: it is the pushforward of the uniform global variable along the classes of those graphons. Thus the Aldous–Hoover representation and the Diaconis–Janson correspondence agree on their mixing measure, independently of the choice of coding or strict graphon representatives.

Every exchangeable graph law admits a coding of its adjacency array with this mixing measure. The coding need not be pointwise symmetric or have a prescribed diagonal: graphLawOfArray symmetrizes its entries and discards its diagonal.

References

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

theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_symm_eq_map_codingGraphon (L : InfiniteExchangeableGraphLaw) {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool} (hf : Measurable f) (hL : graphLawOfArray (MeasureTheory.Measure.map (fun (u : Probability.AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => Probability.AldousHoover.jointArray f p u) (Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ))) = L.law) : graphonMixtureLawEquiv.symm L = MeasureTheory.ProbabilityMeasure.map ⟨MeasureTheory.volume, ⋯⟩ fun (t : ↑unitInterval) => SeparationQuotient.mk (codingGraphon (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q)) ⋯)

The mixing measure of the graph law of a joint coding is the law of the graphon class obtained by freezing its uniform global variable. This identifies the mixing measure for any coding of the graph law, without pointwise symmetry or diagonal assumptions on the coding.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.exists_jointCoding_mixingMeasure (L : InfiniteExchangeableGraphLaw) : ∃ (f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool) (hf : Measurable f), MeasureTheory.Measure.map (fun (u : Probability.AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => Probability.AldousHoover.jointArray f p u) (Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ)) = arrayLaw L.law ∧ graphonMixtureLawEquiv.symm L = MeasureTheory.ProbabilityMeasure.map ⟨MeasureTheory.volume, ⋯⟩ fun (t : ↑unitInterval) => SeparationQuotient.mk (codingGraphon (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q)) ⋯)

Every exchangeable graph law has an Aldous–Hoover coding of its adjacency array whose frozen coding graphons induce exactly its Diaconis–Janson mixing measure.