Empirical mixing measures of an exchangeable graph law

Every exchangeable graph law L produces a sequence of candidate mixing measures on the graphon space over the unit interval: sample an n-vertex graph from the level-n marginal of L and take the graphon class of its step graphon. This is the empirical mixing measure empiricalMixing L n, the pushforward of L.law n along G ↦ ⟦W_G⟧.

The point of these measures is that they recover the upper masses of L in the limit. The average of t(F, ·) against empiricalMixing L n is, for positive n (or an empty pattern), the mean ordinary homomorphism density E[t(F, G)] of an L-sample G on n vertices. Its injective counterpart is exact: by consistency of L, each of the (n)_k vertex embeddings of a k-vertex pattern F sees the pattern with probability upperMass F, so E[t₀(F, G)] = upperMass F whenever k ≤ n. The two densities differ by at most C(k, 2) / n, the union bound on the proportion of non-injective vertex maps, which gives the collision estimate |∫ t(F, ·) d(empiricalMixing L (n + 1)) - upperMass F| ≤ C(k, 2) / (n + 1) and hence convergence of the empirical hom-density averages to the upper masses. Each descended density t(F, ·) is bounded and continuous, so weak convergence carries these averages to any weak limit point P of the empirical mixing measures: the mixture law of P then has the upper masses of L, and since upper masses determine an exchangeable graph law, it is L. This limit identification is how the Diaconis–Janson representation of exchangeable graph laws by graphon mixtures is obtained.

Main definitions

• TauCeti.DenseGraphLimits.empiricalMixing — the graphon class of an n-vertex sample from an exchangeable graph law, as a probability measure on graphon space.

Main results

• TauCeti.DenseGraphLimits.integral_homDensityOnSpace_empiricalMixing — averaging t(F, ·) against an empirical mixing measure is taking the mean homomorphism density of a sample;
• TauCeti.DenseGraphLimits.abs_integral_homDensityOnSpace_empiricalMixing_sub_le — the collision estimate;
• TauCeti.DenseGraphLimits.tendsto_integral_homDensityOnSpace_empiricalMixing — the empirical hom-density averages converge to the upper masses;
• TauCeti.DenseGraphLimits.mixtureExchangeableLaw_eq_of_tendsto_empiricalMixing — every weak limit of the empirical mixing measures along a diverging sequence of sample sizes is a mixing measure for the law.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Sections 5.2 and 11.3.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/MixtureExistence.lean. The empirical mixing measures and the collision estimate follow its existence argument.

noncomputable def TauCeti.DenseGraphLimits.empiricalMixing (L : ExchangeableGraphLaw) (n : ℕ) : MeasureTheory.ProbabilityMeasure GraphonSpaceI

Empirical mixing measures. The graphon class of an n-vertex sample from an exchangeable graph law: the pushforward of the level-n marginal along G ↦ ⟦W_G⟧, where W_G is the step graphon of G on the unit interval.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DenseGraphLimits.toMeasure_empiricalMixing (L : ExchangeableGraphLaw) (n : ℕ) : ↑(empiricalMixing L n) = MeasureTheory.Measure.map (fun (G : SimpleGraph (Fin n)) => SeparationQuotient.mk (finiteGraphGraphon G)) (L.law n)

The empirical mixing measure is the pushforward of the level-n marginal along the graphon class of the step graphon.

theorem TauCeti.DenseGraphLimits.integral_homDensityOnSpace_empiricalMixing (L : ExchangeableGraphLaw) {V : Type u_1} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] {n : ℕ} (hn : Nonempty V → 0 < n) : ∫ (x : GraphonSpaceI), homDensityOnSpace F x ∂↑(empiricalMixing L n) = ∫ (G : SimpleGraph (Fin n)), homDensityFin F G ∂L.law n

Averaging a homomorphism density against an empirical mixing measure is taking the mean homomorphism density of a sample from the law. Positivity of n is needed when V is nonempty, since the finite density of a nonempty pattern in the empty graph is 0; an empty pattern has density 1 on both sides.

theorem TauCeti.DenseGraphLimits.abs_integral_homDensityOnSpace_empiricalMixing_sub_le (L : ExchangeableGraphLaw) (n : ℕ) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : |∫ (x : GraphonSpaceI), homDensityOnSpace F x ∂↑(empiricalMixing L (n + 1)) - L.upperMass F| ≤ ↑(k.choose 2) / (↑n + 1)

The collision estimate. Averaging t(F, ·) against the empirical mixing measure of an exchangeable graph law at sample size n + 1 recovers the upper mass of F up to C(k, 2) / (n + 1), where k is the number of vertices of F.

theorem TauCeti.DenseGraphLimits.tendsto_integral_homDensityOnSpace_empiricalMixing (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : Filter.Tendsto (fun (n : ℕ) => ∫ (x : GraphonSpaceI), homDensityOnSpace F x ∂↑(empiricalMixing L n)) Filter.atTop (nhds (L.upperMass F))

The average of t(F, ·) against the empirical mixing measures of an exchangeable graph law converges to the upper mass of F.

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLaw_eq_of_tendsto_empiricalMixing (L : ExchangeableGraphLaw) {P : MeasureTheory.ProbabilityMeasure GraphonSpaceI} {φ : ℕ → ℕ} (hφ : Filter.Tendsto φ Filter.atTop Filter.atTop) (hconv : Filter.Tendsto (fun (m : ℕ) => empiricalMixing L (φ m)) Filter.atTop (nhds P)) : mixtureExchangeableLaw P = L

Limit identification. A weak limit P of the empirical mixing measures of an exchangeable graph law L, along any diverging sequence of sample sizes, is a mixing measure for L: the mixture law of P is L.