Aldous–Hoover codings of graphs are graphon samples

A jointly exchangeable Aldous–Hoover coding with values in Bool reads off a graph on ℕ: the pair {i, j} is an edge when the coding puts true at (i, j) or at (j, i), the diagonal being ignored. This file identifies the law of that graph with the graphon sampling laws: the graph law of a coding is a mixture of joint sampling laws, and every joint sampling law on the unit interval is the graph law of a coding.

For a coding g : I × I × I → Bool that ignores its global variable, the two entries at (i, j) and (j, i) read the vertex variables U i, U j and the one shared cell variable U {i, j}. Conditionally on the vertex variables, the cells are independent and the pair {i, j} is an edge with probability

codingGraphon g (x, y) = P(g (x, y, ξ) ∨ g (y, x, ξ)),   ξ uniform on I,

at x = U i, y = U j. This is a graphon on (I, volume), symmetric by construction and with no condition on g beyond measurability, and the graph read off the coding has the joint sampling law infiniteSampleLaw (codingGraphon g).

A coding that does use its global variable is a uniform mixture of the codings obtained by freezing that variable (TauCeti.Probability.AldousHoover.map_jointArray_eq_bind_frozen), so its graph law is the corresponding mixture of joint sampling laws. Conversely every graphon W on (I, volume) has a coding, graphonCoding W, which joins two vertices when the cell variable falls below the graphon value, and whose coding graphon is W itself.

Main definitions

• TauCeti.DenseGraphLimits.codingGraphon — the graphon of a global-free Bool-valued coding.
• TauCeti.DenseGraphLimits.graphonCoding — the threshold coding of a graphon on (I, volume).

Main results

• TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray_snd — the graph law of a global-free coding is the joint sampling law of its coding graphon.
• TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray — the graph law of any joint coding is the uniform mixture, over the global variable, of the joint sampling laws of the frozen codings.
• TauCeti.DenseGraphLimits.measurable_codingGraphon — the coding graphons of the frozen codings depend jointly measurably on the frozen variable, so they form a measurable family of graphons.
• TauCeti.DenseGraphLimits.codingGraphon_graphonCoding and TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray_graphonCoding — every graphon on the unit interval is the coding graphon of its threshold coding, so its joint sampling law is the graph law of a coding.

References

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

The coding graphon

noncomputable def TauCeti.DenseGraphLimits.codingGraphon (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool) (hg : Measurable g) : Graphon (↑unitInterval) MeasureTheory.volume

The graphon of a global-free coding. For a coding g of the cell variable from two vertex variables, the value at (x, y) is the probability, over a uniform cell variable t, that g joins x and y in either orientation: g (x, y, t) or g (y, x, t). This is the edge probability of the graph read off the coding, conditionally on the two vertex variables.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DenseGraphLimits.codingGraphon_apply (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool) (hg : Measurable g) (x y : ↑unitInterval) : (codingGraphon g hg) x y = MeasureTheory.volume.real {t : ↑unitInterval | g (x, y, t) = true ∨ g (y, x, t) = true}

The value of the coding graphon is the probability that the coding joins the two vertex values in either orientation.

theorem TauCeti.DenseGraphLimits.measurable_codingGraphon {T : Type u_1} [MeasurableSpace T] {f : T × ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool} (hf : Measurable f) : Measurable fun (p : T × ↑unitInterval × ↑unitInterval) => (codingGraphon (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (p.1, q)) ⋯) p.2.1 p.2.2

Coding graphons depend measurably on a parameter. For a measurable coding f with an extra parameter t, the coding graphon of the frozen coding (x, y, s) ↦ f (t, x, y, s) is jointly measurable in t and its two arguments.

The graph read off a coding

The graph law of a coding

theorem TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray_snd (g : ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool) (hg : Measurable g) : graphLawOfArray (MeasureTheory.Measure.map (fun (u : Probability.AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => Probability.AldousHoover.jointArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => g q.2) p u) (Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ))) = infiniteSampleLaw (codingGraphon g hg)

The graph law of a global-free coding is a joint sampling law. The graph read off the joint Aldous–Hoover coding (i, j) ↦ g (U i, U j, U {i, j}), which ignores the global variable, has the law of the infinite W-random graph for the coding graphon W = codingGraphon g.

theorem TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray {f : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool} (hf : Measurable f) : graphLawOfArray (MeasureTheory.Measure.map (fun (u : Probability.AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => Probability.AldousHoover.jointArray f p u) (Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ))) = MeasureTheory.volume.bind fun (t : ↑unitInterval) => infiniteSampleLaw (codingGraphon (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval) => f (t, q)) ⋯)

The graph law of a joint coding is a mixture of joint sampling laws. The graph read off the joint Aldous–Hoover coding (i, j) ↦ f (U, U i, U j, U {i, j}) has the law obtained by averaging, over a uniform value t of the global variable, the joint sampling law of the coding graphon of the frozen coding (x, y, s) ↦ f (t, x, y, s).

The threshold coding of a graphon

noncomputable def TauCeti.DenseGraphLimits.graphonCoding (W : Graphon (↑unitInterval) MeasureTheory.volume) : ↑unitInterval × ↑unitInterval × ↑unitInterval → Bool

The threshold coding of a graphon on the unit interval. The coding joins two vertices with values x and y when the cell variable falls below the graphon value W x y.

Equations

• TauCeti.DenseGraphLimits.graphonCoding W q = decide (q.2.2 < ⟨W q.1 q.2.1, ⋯⟩)

@[simp]

theorem TauCeti.DenseGraphLimits.graphonCoding_apply (W : Graphon (↑unitInterval) MeasureTheory.volume) (x y t : ↑unitInterval) : graphonCoding W (x, y, t) = decide (↑t < W x y)

The threshold coding is true exactly below the graphon value.

theorem TauCeti.DenseGraphLimits.measurable_graphonCoding (W : Graphon (↑unitInterval) MeasureTheory.volume) : Measurable (graphonCoding W)

The threshold coding of a graphon is measurable.

@[simp]

theorem TauCeti.DenseGraphLimits.codingGraphon_graphonCoding (W : Graphon (↑unitInterval) MeasureTheory.volume) : codingGraphon (graphonCoding W) ⋯ = W

Every graphon on the unit interval is a coding graphon: the coding graphon of the threshold coding of W is W.

theorem TauCeti.DenseGraphLimits.graphLawOfArray_map_jointArray_graphonCoding (W : Graphon (↑unitInterval) MeasureTheory.volume) : graphLawOfArray (MeasureTheory.Measure.map (fun (u : Probability.AldousHoover.NoiseIndex Unit (Sym2 ℕ) → ↑unitInterval) (p : ℕ × ℕ) => Probability.AldousHoover.jointArray (fun (q : ↑unitInterval × ↑unitInterval × ↑unitInterval × ↑unitInterval) => graphonCoding W q.2) p u) (Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ))) = infiniteSampleLaw W

Every joint sampling law on the unit interval is the graph law of a coding: the graph read off the threshold coding of W has the law of the infinite W-random graph.