Expected homomorphism densities in graphon samples

For a fixed finite graph F, the expected ordinary homomorphism density of F in a graphon sample G(n, W) converges to the graphon homomorphism density t(F, W). At every finite sample size n ≥ |V(F)|, the difference is at most |V(F)|.choose 2 / n.

The proof compares the ordinary homomorphism density with the injective density. The injective density is exactly unbiased under graphon sampling, while the two finite densities differ only when a sampled vertex map has a collision.

Main results

• SimpleGraph.abs_integral_homDensityFin_sampleGraph_sub_le bounds the finite-sample bias of the ordinary homomorphism density for samples with at least |V(F)| vertices;
• SimpleGraph.tendsto_integral_homDensityFin_sampleGraph gives convergence of its expectation to the graphon homomorphism density.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Sections 5.2 and 10.1.

theorem SimpleGraph.abs_integral_homDensityFin_sampleGraph_sub_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : TauCeti.DenseGraphLimits.Graphon Ω μ) {n : ℕ} (hVn : Fintype.card V ≤ n) : |∫ (G : SimpleGraph (Fin n)), TauCeti.DenseGraphLimits.homDensityFin F G ∂TauCeti.DenseGraphLimits.sampleGraph W n - TauCeti.DenseGraphLimits.homDensity F W| ≤ ↑((Fintype.card V).choose 2) / ↑n

The mean ordinary homomorphism density differs from the graphon density by no more than the collision probability bound, whenever the sample has enough vertices for the injective density.

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

The expected ordinary homomorphism density of a fixed finite graph in G(n, W) converges to its graphon homomorphism density as the sample size tends to infinity.