Homomorphism densities as coordinates on graphon space

The homomorphism densities of all finite graphs, taken together, form one map from graphon space into a countable product of copies of ℝ. This file shows that this map is a topological embedding of every graphon space.

On the compact space GraphonSpaceI the densities separate points, so they are a continuous injection into a Hausdorff space, hence a closed embedding. Every graphon space embeds isometrically into GraphonSpaceI without changing any homomorphism density, so the density coordinates are an embedding over any probability carrier.

Main definitions

• TauCeti.DenseGraphLimits.homDensityCoords — the homomorphism densities of all graphs on Fin n, as one point of a product of copies of ℝ.

Main results

• TauCeti.DenseGraphLimits.isClosedEmbedding_homDensityCoords — on the unit-interval graphon space, the density coordinates are a closed embedding;
• TauCeti.DenseGraphLimits.isInducing_homDensityCoords — on the graphon space over any probability carrier, the density coordinates are inducing.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Sections 2--3 (graph limits as a compact space coordinatised by homomorphism densities).

noncomputable def TauCeti.DenseGraphLimits.homDensityCoords {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) (p : (n : ℕ) × (F : SimpleGraph (Fin n)) × DecidableRel F.Adj) : ℝ

The homomorphism densities of all finite graphs on Fin n, each with its decidability instance, as one point of a product of copies of ℝ.

Equations

• TauCeti.DenseGraphLimits.homDensityCoords x p = TauCeti.DenseGraphLimits.homDensityOnSpace p.snd.fst x

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityCoords_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) {n : ℕ} (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] : homDensityCoords x ⟨n, ⟨F, inst✝⟩⟩ = homDensityOnSpace F x

Each density coordinate is the homomorphism density of its graph.

theorem TauCeti.DenseGraphLimits.continuous_homDensityCoords {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Continuous homDensityCoords

The density coordinates are continuous: each homomorphism density is.

theorem TauCeti.DenseGraphLimits.injective_homDensityCoords {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Function.Injective homDensityCoords

The density coordinates are injective: homomorphism densities separate graphon classes.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensityCoords_toGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (x : GraphonSpace Ω μ) : homDensityCoords (toGraphonSpaceI x) = homDensityCoords x

Embedding into the unit-interval graphon space does not change the density coordinates.

theorem TauCeti.DenseGraphLimits.isClosedEmbedding_homDensityCoords : Topology.IsClosedEmbedding homDensityCoords

The density coordinates are a closed embedding of GraphonSpaceI. They are a continuous injection of a compact space into a Hausdorff space.

theorem TauCeti.DenseGraphLimits.isInducing_homDensityCoords {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : Topology.IsInducing homDensityCoords

The density coordinates embed every graphon space. Every graphon space embeds isometrically into GraphonSpaceI without changing any density, and there the density coordinates are a closed embedding.