Almost-sure convergence of sampled homomorphism densities

Sample the infinite W-random graph once, from the joint sampling law infiniteSampleLaw W, and read off its growing windows on the labels below n; each window has the law G(n, W). This file shows that, almost surely, the homomorphism densities of the windows converge to those of W: for a fixed finite graph F, and simultaneously for every finite graph on Fin k and every k.

The last form is phrased with the step graphons finiteGraphGraphon of the windows, which are graphons on the unit interval: almost surely every homomorphism density of the windows' step graphons converges to the corresponding density of W. Combined with the equivalence between convergence of all homomorphism densities and convergence in cut distance, this is what yields almost-sure convergence of the windows to W in cut distance.

Main results

• TauCeti.DenseGraphLimits.tendsto_homDensityFin_infiniteSampleLaw_ae — for a fixed finite graph F, the homomorphism densities of the windows converge to t(F, W) almost surely.
• TauCeti.DenseGraphLimits.tendsto_homDensityFin_infiniteSampleLaw_ae_forall — almost surely this holds for every graph on Fin k, simultaneously for all k.
• TauCeti.DenseGraphLimits.tendsto_homDensity_finiteGraphGraphon_infiniteSampleLaw_ae_forall — the same statement for the step graphons of the windows.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §10.1.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/AlmostSureSampling.lean, whose proof route is adapted here.

theorem TauCeti.DenseGraphLimits.tendsto_homDensityFin_infiniteSampleLaw_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, Filter.Tendsto (fun (n : ℕ) => homDensityFin F (G.restrictFin n)) Filter.atTop (nhds (homDensity F W))

Almost-sure convergence of a sampled homomorphism density. For a fixed finite graph F, almost every infinite W-random graph G has windows whose homomorphism densities converge to the graphon density:

t(F, G[{0, …, n - 1}]) → t(F, W) as n → ∞.

theorem TauCeti.DenseGraphLimits.tendsto_homDensityFin_infiniteSampleLaw_ae_forall {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], Filter.Tendsto (fun (n : ℕ) => homDensityFin F (G.restrictFin n)) Filter.atTop (nhds (homDensity F W))

Almost-sure convergence of all sampled homomorphism densities. Almost every infinite W-random graph G has windows whose homomorphism densities converge to those of W, for every finite graph on Fin k and every k at once.

theorem TauCeti.DenseGraphLimits.tendsto_homDensity_finiteGraphGraphon_infiniteSampleLaw_ae_forall {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ∀ᵐ (G : SimpleGraph ℕ) ∂infiniteSampleLaw W, ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], Filter.Tendsto (fun (n : ℕ) => homDensity F (finiteGraphGraphon (G.restrictFin (n + 1)))) Filter.atTop (nhds (homDensity F W))

Almost-sure convergence of the sampled step graphons' homomorphism densities. Almost every infinite W-random graph G has windows G[{0, …, n}] whose step graphons on the unit interval satisfy t(F, W_{G[{0, …, n}]}) → t(F, W) for every finite graph F on Fin k and every k at once. The window has n + 1 vertices, so the step graphon is defined for every n.