Unbiased injective homomorphism densities

The injective homomorphism density of a finite pattern in a graph sampled from a graphon is an unbiased estimator of the graphon's homomorphism density. The proof first establishes the basic upper-event identity: the total sampling mass of all supergraphs of F is t(F, W). It then averages that identity over every embedding of the pattern's vertices into the sampled vertex set.

The falling factorial counts ordered vertex embeddings and therefore matches the injective maps in the numerator of injHomDensity. The hypothesis that the sample contains at least as many vertices as the pattern makes this denominator nonzero.

Main results

• TauCeti.DenseGraphLimits.sum_sampleMass_supergraph_eq_homDensity — the probability that the sample contains every edge of F is t(F, W);
• TauCeti.DenseGraphLimits.integral_injHomDensity_eq_sum_div — the average of the injective homomorphism density against any finite measure on host graphs, as an average over vertex embeddings of the mass of the hosts containing the embedded pattern;
• TauCeti.DenseGraphLimits.integral_injHomDensity_eq_of_forall — if every embedded copy of the pattern has the same host mass c, the average injective homomorphism density is c;
• TauCeti.DenseGraphLimits.abs_integral_homDensityFin_sub_integral_injHomDensity_le — under any probability measure on host graphs, the mean ordinary and injective homomorphism densities differ by at most C(k, 2) / n;
• TauCeti.DenseGraphLimits.integral_injHomDensity_sampleGraph — injective homomorphism density is unbiased under graphon sampling.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Sections 5.2 and 10.2.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/Sampling.lean. The supergraph-mass proof is adapted from its Boolean-cube argument to Tau Ceti's strict graphon carrier.

theorem TauCeti.DenseGraphLimits.sum_sampleMass_supergraph_eq_homDensity {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] : ∑ G : SimpleGraph (Fin n) with F ≤ G, sampleMass W G = homDensity F W

The total mass of all sampled graphs containing a fixed graph F is its graphon homomorphism density. Equivalently, the probability that every edge of F appears in the sample is t(F, W).

theorem TauCeti.DenseGraphLimits.integral_injHomDensity_eq_sum_div {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (F : SimpleGraph V) (ν : MeasureTheory.Measure (SimpleGraph W)) [MeasureTheory.IsFiniteMeasure ν] : ∫ (G : SimpleGraph W), injHomDensity F G ∂ν = (∑ f : V ↪ W, ν.real {G : SimpleGraph W | SimpleGraph.map (⇑f) F ≤ G}) / ↑((Fintype.card W).descFactorial (Fintype.card V))

Averaging the injective homomorphism density of a fixed pattern against any finite measure on host graphs averages, over the vertex embeddings of the pattern, the mass of the hosts that contain the embedded pattern.

theorem TauCeti.DenseGraphLimits.integral_injHomDensity_eq_of_forall {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (F : SimpleGraph V) (ν : MeasureTheory.Measure (SimpleGraph W)) [MeasureTheory.IsFiniteMeasure ν] {c : ℝ} (hVW : Fintype.card V ≤ Fintype.card W) (h : ∀ (f : V ↪ W), ν.real {G : SimpleGraph W | SimpleGraph.map (⇑f) F ≤ G} = c) : ∫ (G : SimpleGraph W), injHomDensity F G ∂ν = c

If every embedded copy of a pattern is contained in hosts of the same mass c, the average injective homomorphism density of the pattern is c, provided the host has at least as many vertices as the pattern.

theorem TauCeti.DenseGraphLimits.abs_integral_homDensityFin_sub_integral_injHomDensity_le {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (F : SimpleGraph V) (ν : MeasureTheory.Measure (SimpleGraph W)) [MeasureTheory.IsProbabilityMeasure ν] : |∫ (G : SimpleGraph W), homDensityFin F G ∂ν - ∫ (G : SimpleGraph W), injHomDensity F G ∂ν| ≤ ↑((Fintype.card V).choose 2) / ↑(Fintype.card W)

Under any probability measure on host graphs, the mean ordinary and injective homomorphism densities of a pattern differ by at most C(k, 2) / n, the union bound on the proportion of non-injective vertex maps, where k and n are the numbers of pattern and host vertices.

theorem TauCeti.DenseGraphLimits.integral_injHomDensity_sampleGraph {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] {m : ℕ} (hkm : Fintype.card V ≤ m) : ∫ (G : SimpleGraph (Fin m)), injHomDensity F G ∂sampleGraph W m = homDensity F W

The injective homomorphism density of a graphon sample is an unbiased estimator of the graphon's homomorphism density, provided the sample has at least as many vertices as the pattern. The size condition is exactly the nonvanishing condition for the falling-factorial denominator.