Edge coordinates of an infinite simple graph

An infinite simple graph is equivalently a Boolean assignment to the unordered, non-diagonal pairs of natural numbers. This file makes that equivalence measurable and records its equivariance under relabelling. It is the carrier-level bridge between laws on infinite simple graphs and laws on jointly exchangeable symmetric, irreflexive Boolean arrays.

Finite measures on infinite graphs are determined by the laws of all their finite vertex windows: every finite collection of edge coordinates lies in one such window, so projective-limit uniqueness applies after transporting the measures through the coordinate equivalence.

The coordinate type excludes diagonal pairs, rather than imposing an irreflexivity condition on a two-dimensional array. Consequently every Boolean assignment is a graph, and relabelling acts by an honest equivalence of coordinates.

Main definitions

• TauCeti.DenseGraphLimits.EdgeIndex is the type of unordered non-diagonal pairs of naturals;
• TauCeti.DenseGraphLimits.graphCoordEquiv identifies infinite graphs with Boolean edge coordinates;
• Equiv.Perm.edgeIndexMap is the coordinate relabelling induced by a permutation of the vertices.

Main results

• TauCeti.DenseGraphLimits.measurable_graphCoordEquiv and TauCeti.DenseGraphLimits.measurable_graphCoordEquiv_symm show that the coordinate equivalence is measurable in both directions;
• TauCeti.DenseGraphLimits.measure_ext_of_map_restrictFin shows that a finite measure on infinite graphs is determined by its finite windows;
• Equiv.Perm.graphCoordEquiv_comap is the relabelling commuting square.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 4.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteGraph.lean. The off-diagonal coordinate representation and relabelling square follow that source, adapted here to Mathlib's existing measurable space on SimpleGraph ℕ.

@[reducible, inline]

abbrev TauCeti.DenseGraphLimits.EdgeIndex : Type

The coordinate type of an infinite simple graph: unordered pairs of distinct naturals.

Equations

• TauCeti.DenseGraphLimits.EdgeIndex = { e : Sym2 ℕ // ¬e.IsDiag }

noncomputable def TauCeti.DenseGraphLimits.graphCoordEquiv : SimpleGraph ℕ ≃ (EdgeIndex → Bool)

An infinite simple graph is equivalently a Boolean assignment to its possible edges.

Equations

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

@[simp]

theorem SimpleGraph.graphCoordEquiv_apply (G : SimpleGraph ℕ) (e : TauCeti.DenseGraphLimits.EdgeIndex) : TauCeti.DenseGraphLimits.graphCoordEquiv G e = true ↔ ↑e ∈ G.edgeSet

The coordinate at e is true exactly when e is an edge of the graph.

@[simp]

theorem TauCeti.DenseGraphLimits.mem_edgeSet_graphCoordEquiv_symm (f : EdgeIndex → Bool) (e : EdgeIndex) : ↑e ∈ (graphCoordEquiv.symm f).edgeSet ↔ f e = true

An edge coordinate is an edge of the decoded graph exactly when its value is true.

theorem TauCeti.DenseGraphLimits.measurable_graphCoordEquiv : Measurable ⇑graphCoordEquiv

The graph-to-coordinate map is measurable for Mathlib's adjacency-generated measurable space on simple graphs and the product measurable space on Boolean coordinates.

theorem TauCeti.DenseGraphLimits.measurable_graphCoordEquiv_symm : Measurable ⇑graphCoordEquiv.symm

The coordinate-to-graph map is measurable, so graphCoordEquiv is a measurable equivalence in substance.

Edge-coordinate windows

def TauCeti.DenseGraphLimits.edgeWindow (n : ℕ) : Finset EdgeIndex

The edge coordinates both of whose endpoints are below n.

Equations

• TauCeti.DenseGraphLimits.edgeWindow n = Finset.subtype (fun (e : Sym2 ℕ) => ¬e.IsDiag) (Finset.range n).sym2

@[simp]

theorem TauCeti.DenseGraphLimits.mem_edgeWindow {n : ℕ} {e : EdgeIndex} : e ∈ edgeWindow n ↔ ∀ a ∈ ↑e, a < n

Membership in edgeWindow n means that both endpoints are below n.

def TauCeti.DenseGraphLimits.windowBound (J : Finset EdgeIndex) : ℕ

A bound below which all endpoints of the coordinates in J lie.

Equations

• TauCeti.DenseGraphLimits.windowBound J = J.sup fun (e : TauCeti.DenseGraphLimits.EdgeIndex) => (↑e).sup + 1

theorem TauCeti.DenseGraphLimits.subset_edgeWindow_windowBound (J : Finset EdgeIndex) : J ⊆ edgeWindow (windowBound J)

Every coordinate in a finite set lies in the window at its windowBound.

noncomputable def TauCeti.DenseGraphLimits.windowCoord {n : ℕ} (H : SimpleGraph (Fin n)) : EdgeIndex → Bool

The edge coordinates of a graph on Fin n, with its labels read in ℕ.

Equations

• TauCeti.DenseGraphLimits.windowCoord H = TauCeti.DenseGraphLimits.graphCoordEquiv (SimpleGraph.map (⇑Fin.valEmbedding) H)

@[simp]

theorem TauCeti.DenseGraphLimits.windowCoord_apply {n : ℕ} (H : SimpleGraph (Fin n)) (e : EdgeIndex) : windowCoord H e = graphCoordEquiv (SimpleGraph.map (⇑Fin.valEmbedding) H) e

A finite graph's window coordinates are those of its embedding into the natural labels.

theorem TauCeti.DenseGraphLimits.graphCoordEquiv_eq_windowCoord {n : ℕ} (G : SimpleGraph ℕ) {e : EdgeIndex} (he : e ∈ edgeWindow n) : graphCoordEquiv G e = windowCoord (G.restrictFin n) e

Below a bound, the edge coordinates of an infinite graph are read off its window.

Finite measures on infinite graphs are determined by their windows

theorem TauCeti.DenseGraphLimits.measure_ext_of_map_restrictFin {μ ν : MeasureTheory.Measure (SimpleGraph ℕ)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin n) μ = MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin n) ν) : μ = ν

A finite measure on the graphs on ℕ is determined by its windows. The coordinates of an infinite graph below any bound are a function of its window, so the laws of all finitely many coordinates agree, and the law of the coordinates is their unique projective limit.

def Equiv.Perm.edgeIndexMap (e : Perm ℕ) : TauCeti.DenseGraphLimits.EdgeIndex ≃ TauCeti.DenseGraphLimits.EdgeIndex

A permutation of the vertices relabels the unordered non-diagonal edge coordinates.

Equations

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

@[simp]

theorem Equiv.Perm.edgeIndexMap_val (e : Perm ℕ) (p : TauCeti.DenseGraphLimits.EdgeIndex) : ↑(e.edgeIndexMap p) = Sym2.map ⇑e ↑p

Vertex relabelling acts on an edge coordinate by applying the permutation to both endpoints.

@[simp]

theorem Equiv.Perm.edgeIndexMap_refl : edgeIndexMap (Equiv.refl ℕ) = Equiv.refl TauCeti.DenseGraphLimits.EdgeIndex

The identity vertex relabelling induces the identity edge-coordinate relabelling.

@[simp]

theorem Equiv.Perm.edgeIndexMap_trans (e₁ e₂ : Perm ℕ) : edgeIndexMap (Equiv.trans e₁ e₂) = e₁.edgeIndexMap.trans e₂.edgeIndexMap

Successive vertex relabellings induce the corresponding successive coordinate relabellings.

@[simp]

theorem Equiv.Perm.edgeIndexMap_symm (e : Perm ℕ) : e.edgeIndexMap.symm = edgeIndexMap (Equiv.symm e)

Inverting a vertex relabelling inverts the induced edge-coordinate relabelling.

@[simp]

theorem Equiv.Perm.graphCoordEquiv_comap (e : Perm ℕ) (G : SimpleGraph ℕ) (p : TauCeti.DenseGraphLimits.EdgeIndex) : TauCeti.DenseGraphLimits.graphCoordEquiv (SimpleGraph.comap (⇑e) G) p = TauCeti.DenseGraphLimits.graphCoordEquiv G (e.edgeIndexMap p)

Relabelling an infinite graph is the same as relabelling its Boolean edge coordinates.