Summable tails for sampled homomorphism densities

For a fixed finite graph and a positive tolerance, the probabilities that its homomorphism density in a graphon sample deviates from the graphon density have finite total mass. This is the summability input needed to apply the first Borel--Cantelli lemma to the restrictions of a single infinite graphon sample.

The proof uses the exponential concentration estimate for all sufficiently large sample sizes. The empty pattern is handled separately: both densities are identically one, so every deviation event is empty.

Main result

• SimpleGraph.tsum_sampleGraph_homDensityFin_tail_ne_top — the deviation probabilities at sample sizes n + 1 have finite sum.

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/SampleExposure.lean. The split between the empty-pattern case and the eventually exponential tail follows that file.

theorem SimpleGraph.tsum_sampleGraph_homDensityFin_tail_ne_top {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : TauCeti.DenseGraphLimits.Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) : ∑' (n : ℕ), (TauCeti.DenseGraphLimits.sampleGraph W (n + 1)) {G : SimpleGraph (Fin (n + 1)) | ε ≤ |TauCeti.DenseGraphLimits.homDensityFin F G - TauCeti.DenseGraphLimits.homDensity F W|} ≠ ⊤

For a fixed finite graph F and ε > 0, the probabilities

P(|t(F, G(n + 1, W)) - t(F, W)| ≥ ε)

have finite total mass. Thus the corresponding events on the joint infinite sampling space are eligible for the first Borel--Cantelli lemma.