Measurability of individual simple graphs and of relabelling

Mathlib equips SimpleGraph V with the sigma-algebra induced by all adjacency coordinates. When V is countable, an individual graph is measurable because its edge set is a measurable point in the countable product space. This supplies the discrete integration API for finite random graphs.

Each adjacency coordinate of a graph pulled back along a map of vertex types is a single adjacency coordinate of the source graph, so the pullback is measurable with no hypothesis on either vertex type. This is what lets a random graph be restricted to a window of labels: the window SimpleGraph.restrictFin is the special case along Fin.val.

For graphs on ℕ the windows carve out the window cylinders, the events that a prescribed finite window occurs. Two cylinders meet in a cylinder, and every adjacency coordinate is read off a long enough window, so the cylinders are a π-system generating the sigma-algebra. That is the test family for the two standard reductions on infinite graphs: a finite measure is determined by its values on cylinders, and a family of probability measures is measurable once its cylinder masses are.

Main definitions

• SimpleGraph.restrictFinCylinders — the window cylinders of graphs on ℕ.

Main results

• SimpleGraph.instMeasurableSingletonClass — singletons of graphs on a countable vertex type are measurable;
• SimpleGraph.measurable_comap — pulling back along a map of vertex types is measurable;
• SimpleGraph.measurable_restrictFin — taking a window is measurable;
• SimpleGraph.isPiSystem_restrictFinCylinders and SimpleGraph.generateFrom_restrictFinCylinders — the window cylinders are a π-system generating the sigma-algebra on SimpleGraph ℕ.

Reference

• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/SamplingLaw.lean. The instance is adapted from its measurable singleton instance; the proof here goes through Mathlib's SimpleGraph.measurableEmbedding_edgeSet.

instance SimpleGraph.instMeasurableSingletonClass {V : Type u_1} [Countable V] : MeasurableSingletonClass (SimpleGraph V)

The canonical measurable space on simple graphs over a countable vertex type has measurable singletons.

theorem SimpleGraph.measurable_comap {V : Type u_1} {W : Type u_2} (f : V → W) : Measurable (SimpleGraph.comap f)

Pulling a simple graph back along a map of vertex types is measurable: each adjacency coordinate of the pullback is an adjacency coordinate of the source.

theorem SimpleGraph.measurable_restrictFin (n : ℕ) : Measurable fun (G : SimpleGraph ℕ) => G.restrictFin n

Taking a window is measurable.

theorem SimpleGraph.measurable_adjArray {V : Type u_3} : Measurable adjArray

Reading a graph as its adjacency array is measurable.

Window cylinders

def SimpleGraph.restrictFinCylinders : Set (Set (SimpleGraph ℕ))

The window cylinders of graphs on ℕ: the events that the window spanned by the first n labels is a prescribed finite graph.

Equations

• SimpleGraph.restrictFinCylinders = {s : Set (SimpleGraph ℕ) | ∃ (n : ℕ) (H : SimpleGraph (Fin n)), s = (fun (G : SimpleGraph ℕ) => G.restrictFin n) ⁻¹' {H}}

theorem SimpleGraph.mem_restrictFinCylinders {s : Set (SimpleGraph ℕ)} : s ∈ restrictFinCylinders ↔ ∃ (n : ℕ) (H : SimpleGraph (Fin n)), s = (fun (G : SimpleGraph ℕ) => G.restrictFin n) ⁻¹' {H}

Membership in the window cylinders unfolds to a window and a prescribed finite graph.

theorem SimpleGraph.preimage_restrictFin_mem_restrictFinCylinders (n : ℕ) (H : SimpleGraph (Fin n)) : (fun (G : SimpleGraph ℕ) => G.restrictFin n) ⁻¹' {H} ∈ restrictFinCylinders

The event that the length-n window is H is a window cylinder.

theorem SimpleGraph.measurableSet_of_mem_restrictFinCylinders {s : Set (SimpleGraph ℕ)} (hs : s ∈ restrictFinCylinders) : MeasurableSet s

Window cylinders are measurable, since taking a window is measurable and singletons of finite graphs are measurable.

theorem SimpleGraph.isPiSystem_restrictFinCylinders : IsPiSystem restrictFinCylinders

The window cylinders are a π-system. Of two cylinders that meet, the one at the longer window is contained in the other, because the shorter window is a window of the longer one.

theorem SimpleGraph.generateFrom_restrictFinCylinders : MeasurableSpace.generateFrom restrictFinCylinders = inferInstance

The window cylinders generate the sigma-algebra on infinite graphs. Every adjacency coordinate is read off the window spanned by the first max u v + 1 labels, and that window takes countably many values.