Concentration of sampled homomorphism densities

For a fixed finite graph F, its ordinary homomorphism density in a graphon sample G(n, W) concentrates exponentially around the graphon homomorphism density. The proof applies McDiarmid's bounded-differences inequality to the padded vertex exposure: its coordinates are independent, its pushforward is the sampling law, and changing one coordinate moves the density by at most |V(F)| / n.

McDiarmid centers the estimator at its finite-sample mean. The ordinary density is not exactly unbiased because vertex maps may collide, so the proof compares it to the injective density. The latter is unbiased, while their pointwise difference is at most |V(F)|.choose 2 / n. The stated side condition absorbs this collision bias.

Main result

• TauCeti.DenseGraphLimits.sampleGraph_homDensityFin_concentration — the probability of a deviation of at least ε is at most 2 * exp (-ε²n / (2|V(F)|²)).

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 centering, collision-bias transfer, and two-tail calculation are adapted from that file.

theorem TauCeti.DenseGraphLimits.sampleGraph_homDensityFin_concentration {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) {n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : 2 * ↑(Fintype.card V) ^ 2 ≤ ε * ↑n) : ((sampleGraph W n) {G : SimpleGraph (Fin n) | ε ≤ |homDensityFin F G - homDensity F W|}).toReal ≤ 2 * Real.exp (-(ε ^ 2 * ↑n) / (2 * ↑(Fintype.card V) ^ 2))

Exponential concentration of a sampled homomorphism density. Let F have q vertices. If 2q² ≤ εn, then under the graphon sampling law G(n, W),

P(|t(F, G(n, W)) - t(F, W)| ≥ ε) ≤ 2 exp(-ε²n / (2q²)).

The side condition is eventual in n for fixed F and positive ε; it absorbs the collision bias between the mean ordinary homomorphism density and the graphon density.