Graphon mixtures of exchangeable graph laws

A probability measure P on graphon space describes a two-stage random graph: first draw a graphon class ⟦W⟧ ∼ P, then sample G(k, W). This file makes that construction precise and packages its marginals as an exchangeable graph law, the object direction of the Diaconis–Janson correspondence between exchangeable random graphs and mixtures of graphons.

The second stage must depend only on the graphon class, and it does: the law of G(k, W) is determined by its upper masses, which are the homomorphism densities of W, and those are unchanged at cut distance zero. So sampling descends to a map from graphon space to laws of finite graphs. That map is measurable for the Borel σ-algebra of the cut metric, because on the finite lattice of graphs a law is measurable in a parameter once its upper-ray masses are, and those masses are the continuous descended homomorphism densities. The mixture law at level k is the Giry-monad bind of P against this map. Its consistency under relabelling is inherited fiberwise from the sampling laws, its upper mass of a pattern F is the P-average of t(F, ·), and the mixture of a Dirac mass at ⟦W⟧ is the sampling law of W.

Main definitions

• TauCeti.DenseGraphLimits.sampleGraphOnSpace — the law of the sampled graph, as a function of the graphon class;
• TauCeti.DenseGraphLimits.mixtureExchangeableLaw — the exchangeable graph law of a mixing measure on graphon space.

Main results

• TauCeti.DenseGraphLimits.sampleGraph_eq_of_cutDist_eq_zero and TauCeti.DenseGraphLimits.sampleExchangeableLaw_eq_of_cutDist_eq_zero — graphons at cut distance zero, on arbitrary carriers, have the same sampling laws;
• TauCeti.DenseGraphLimits.measurable_sampleGraphOnSpace — the sampling law depends measurably on the graphon class;
• TauCeti.DenseGraphLimits.upperMass_mixtureExchangeableLaw — the upper mass of a pattern under a mixture law is the average of its homomorphism density against the mixing measure;
• TauCeti.DenseGraphLimits.mixtureExchangeableLaw_diracProba — the mixture of a Dirac mass at a graphon class is that graphon's sampling law;
• TauCeti.DenseGraphLimits.mixtureExchangeableLaw_eq_iff — two mixing measures have the same mixture law exactly when they have the same homomorphism-density moments.

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), Section 11.3.

theorem TauCeti.DenseGraphLimits.sampleGraph_eq_of_cutDist_eq_zero {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (h : cutDist U W = 0) (n : ℕ) : sampleGraph U n = sampleGraph W n

Sampling laws are invariant at cut distance zero. Two graphons, on arbitrary probability carriers, at cut distance zero have the same sampling laws: a law on the finite lattice of graphs is determined by its upper-ray masses, which are homomorphism densities.

theorem TauCeti.DenseGraphLimits.sampleExchangeableLaw_eq_of_cutDist_eq_zero {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (h : cutDist U W = 0) : sampleExchangeableLaw U = sampleExchangeableLaw W

Two graphons, on arbitrary probability carriers, at cut distance zero have the same exchangeable sampling law.

noncomputable def TauCeti.DenseGraphLimits.sampleGraphOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : GraphonSpace Ω μ → MeasureTheory.Measure (SimpleGraph (Fin n))

The law of the n-vertex sampled graph as a function of the graphon class. It is well defined because sampling laws are invariant at cut distance zero.

Equations

• TauCeti.DenseGraphLimits.sampleGraphOnSpace n = SeparationQuotient.lift (fun (x : TauCeti.DenseGraphLimits.Graphon Ω μ) => TauCeti.DenseGraphLimits.sampleGraph x n) ⋯

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraphOnSpace_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (W : Graphon Ω μ) : sampleGraphOnSpace n (SeparationQuotient.mk W) = sampleGraph W n

On a representative, the descended sampling law is the sampling law.

instance TauCeti.DenseGraphLimits.isProbabilityMeasure_sampleGraphOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (x : GraphonSpace Ω μ) : MeasureTheory.IsProbabilityMeasure (sampleGraphOnSpace n x)

A sample from a graphon class has a probability law.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraphOnSpace_Ici {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] (x : GraphonSpace Ω μ) : (sampleGraphOnSpace n x) (Set.Ici F) = ENNReal.ofReal (homDensityOnSpace F x)

The probability that a sample from a graphon class contains a pattern is the descended homomorphism density.

theorem TauCeti.DenseGraphLimits.measurable_sampleGraphOnSpace {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : Measurable (sampleGraphOnSpace n)

The sampling law depends measurably on the graphon class. Its upper-ray masses are the continuous descended homomorphism densities, and on the finite lattice of graphs these control every evaluation.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraphOnSpace_map_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (f : Fin k ↪ Fin l) (x : GraphonSpace Ω μ) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑f) (sampleGraphOnSpace l x) = sampleGraphOnSpace k x

The descended sampling laws are consistent under restriction along every injection of labels.

noncomputable def TauCeti.DenseGraphLimits.mixtureExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) : ExchangeableGraphLaw

The mixture map. The exchangeable graph law of a mixing measure P on graphon space: draw a graphon class from P, then sample from it. The level-k marginal is the bind of P against the descended sampling law.

Equations

• TauCeti.DenseGraphLimits.mixtureExchangeableLaw P = { law := fun (k : ℕ) => (↑P).bind (TauCeti.DenseGraphLimits.sampleGraphOnSpace k), prob := ⋯, consistent := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLaw_law {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) (k : ℕ) : (mixtureExchangeableLaw P).law k = (↑P).bind (sampleGraphOnSpace k)

The level-k marginal of a mixture law is the bind of the mixing measure against the descended sampling law.

@[simp]

theorem TauCeti.DenseGraphLimits.upperMass_mixtureExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : (mixtureExchangeableLaw P).upperMass F = ∫ (x : GraphonSpace Ω μ), homDensityOnSpace F x ∂↑P

The coordinate law of a mixture. The upper mass of a pattern under the mixture law of P is the P-average of the pattern's descended homomorphism density: upperMass F = ∫ t(F, ·) dP.

@[simp]

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLaw_diracProba {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : mixtureExchangeableLaw (MeasureTheory.diracProba (SeparationQuotient.mk W)) = sampleExchangeableLaw W

Dirac fibers of the mixture map. Mixing against the Dirac mass at a graphon class samples from that class.

theorem TauCeti.DenseGraphLimits.mixtureExchangeableLaw_eq_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {P Q : MeasureTheory.ProbabilityMeasure (GraphonSpace Ω μ)} : mixtureExchangeableLaw P = mixtureExchangeableLaw Q ↔ ∀ g ∈ homDensitySubmonoid, ∫ (x : GraphonSpace Ω μ), g x ∂↑P = ∫ (x : GraphonSpace Ω μ), g x ∂↑Q

The mixture law records exactly the homomorphism-density moments. Two mixing measures on graphon space have the same mixture law iff they give the same integral to every member of the homomorphism-density submonoid, that is, to every t(F, ·).