Almost-sure convergence of sampled graphons

The growing finite windows of one infinite graph sampled from a graphon converge almost surely to that graphon in cut distance. The generating graphon may have any probability carrier. Equivalently, the windows converge in the metric quotient GraphonSpaceI to the image of the graphon's class under the isometric embedding toGraphonSpaceI; for a graphon on the unit interval, that image is its own class.

This is the simultaneous strong law for homomorphism densities, since convergence in cut distance is convergence of all homomorphism densities (tendsto_cutDist_iff_forall_homDensity_tendsto).

References

• L. Lovász, Large Networks and Graph Limits (2012), §10.1 and Theorem 11.5.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_ae_tendsto_cutDist {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, Filter.Tendsto (fun (n : ℕ) => cutDist (finiteGraphGraphon (G.restrictFin n)) W) Filter.atTop (nhds 0)

Almost every infinite W-random graph has finite windows converging to W in cut distance. No standard-Borel or atomlessness assumption is needed on the generating probability space.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_ae_tendsto_toGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, Filter.Tendsto (fun (n : ℕ) => SeparationQuotient.mk (finiteGraphGraphon (G.restrictFin (n + 1)))) Filter.atTop (nhds (toGraphonSpaceI (SeparationQuotient.mk W)))

The growing nonempty windows of almost every infinite W-random graph converge in GraphonSpaceI to the image of the class of W under the isometric embedding toGraphonSpaceI, for a graphon W on any probability carrier.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_ae_tendsto_graphonSpace (W : Graphon (↑unitInterval) MeasureTheory.volume) : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, Filter.Tendsto (fun (n : ℕ) => SeparationQuotient.mk (finiteGraphGraphon (G.restrictFin (n + 1)))) Filter.atTop (nhds (SeparationQuotient.mk W))

On the unit interval, the growing nonempty sampled windows converge almost surely in graphon space to the class of the generating graphon.