Measurable maps into graphon space

Graphon space carries the Borel σ-algebra of the cut metric. This file shows that the homomorphism densities are a complete set of measurable coordinates for it: a map into graphon space is measurable exactly when each of its homomorphism densities is. This holds over every probability carrier, with no standard-Borel hypothesis.

The reason is topological. The homomorphism densities of all finite graphs are a topological embedding of every graphon space into a countable product of copies of ℝ (isInducing_homDensityCoords), and an embedding pulls the Borel σ-algebra back to the Borel σ-algebra.

The criterion turns joint measurability into measurability of the class: if (t, x, y) ↦ W t x y is measurable, then each density t ↦ t(F, W t) is measurable (measurable_homDensity), so t ↦ ⟦W t⟧ is measurable. This is what makes the law of the class of a random graphon, the pushforward of a measure on the parameter space, a mixing measure on graphon space.

Main results

• TauCeti.DenseGraphLimits.measurable_graphonSpace_iff_forall_homDensity — a map into graphon space is measurable if and only if all its homomorphism densities are;
• TauCeti.DenseGraphLimits.measurable_graphonSpace_mk — the class of a jointly measurable family of graphons is measurable in the parameter.

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).

theorem TauCeti.DenseGraphLimits.measurable_graphonSpace_iff_forall_homDensity {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Type u_2} [MeasurableSpace T] {g : T → GraphonSpace Ω μ} : Measurable g ↔ ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], Measurable fun (t : T) => homDensityOnSpace F (g t)

Homomorphism densities are measurable coordinates on graphon space. A map into graphon space, over any probability carrier, is measurable if and only if the homomorphism density of every finite graph along it is measurable.

theorem TauCeti.DenseGraphLimits.measurable_graphonSpace_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {T : Type u_2} [MeasurableSpace T] {W : T → Graphon Ω μ} (hW : Measurable fun (p : T × Ω × Ω) => (W p.1) p.2.1 p.2.2) : Measurable fun (t : T) => SeparationQuotient.mk (W t)

The class of a measurable family of graphons is measurable. If a family of graphons depends jointly measurably on a parameter, then its class in graphon space depends measurably on the parameter.