Graphons given by a matrix on a countable carrier

On a countable discrete probability carrier there is nothing to a graphon beyond a symmetric [0, 1]-valued matrix: measurability is automatic. Graphon.ofMatrix packages such a matrix as a graphon, with the vertex weights carried by the measure and the edge weights by the matrix. When the carrier is finite this is a weighted graph in the terminology of the graph-limit literature, but nothing here needs finiteness.

The point of the construction is that these carriers are the values a graphon takes once it has been coarsened: a graphon whose value at (x, y) depends on x and y only through a measurable map g : Ω → κ into such a carrier is exactly the pullback of a matrix along g, which is exists_ofMatrix_eq_comap_of_factorsThrough. Step graphons are the case where g is the part-index map of a measurable finite partition, so a step graphon is the pullback of its block matrix and the cut distance to it is a cut distance to a finite object.

Main definitions

• TauCeti.DenseGraphLimits.Graphon.ofMatrix -- the graphon of a symmetric [0, 1]-valued matrix on a countable discrete probability carrier.

Main results

• TauCeti.DenseGraphLimits.exists_ofMatrix_eq_comap_of_factorsThrough -- a graphon whose value depends only on the image of its two arguments under a measurable map into a countable discrete space is the pullback of a matrix along that map.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.1 and §9.2.

def TauCeti.DenseGraphLimits.Graphon.ofMatrix {κ : Type u_1} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (ν : MeasureTheory.Measure κ) [MeasureTheory.IsProbabilityMeasure ν] (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i) : Graphon κ ν

The graphon of a symmetric [0, 1]-valued matrix b on a countable discrete probability carrier (κ, ν), with ν carrying the vertex weights and b the edge weights. For a finite carrier this is the graphon of a weighted graph.

Nothing has to be checked beyond symmetry and the range constraint: every function out of a countable discrete space is measurable.

Equations

• TauCeti.DenseGraphLimits.Graphon.ofMatrix ν b hb = { toFun := fun (i j : κ) => ↑(b i j), symm' := ⋯, meas' := ⋯, bdd' := ⋯, mem01' := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.ofMatrix_apply {κ : Type u_1} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (ν : MeasureTheory.Measure κ) [MeasureTheory.IsProbabilityMeasure ν] (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i) (i j : κ) : (ofMatrix ν b hb) i j = ↑(b i j)

theorem TauCeti.DenseGraphLimits.exists_ofMatrix_eq_comap_of_factorsThrough {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {κ : Type u_2} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] {ν : MeasureTheory.Measure κ} [MeasureTheory.IsProbabilityMeasure ν] (W : Graphon Ω μ) {g : Ω → κ} (hg : Measurable g) (hfac : ∀ (x y x' y' : Ω), g x = g x' → g y = g y' → W x y = W x' y') : ∃ (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i), W = (Graphon.ofMatrix ν b hb).comap g hg μ

A graphon whose value at (x, y) depends on x and y only through a measurable map g into a countable discrete carrier is the pullback along g of a matrix on that carrier. The vertex weights ν are arbitrary: only the underlying function is being rebuilt.

The matrix is existentially quantified because it is only determined on the range of g: outside the range any symmetric completion does, and the one produced here reads the value at an arbitrary g-preimage.