The exchangeable graph law of a graph parameter

A graph parameter f satisfying the four structural conditions of the Lovász–Szegedy representability theorem — isomorphism invariance, multiplicativity, normalization and reflection positivity — defines a random graph: its level-n law gives each graph H on Fin n the Möbius mass f†(H). The Möbius masses are nonnegative and sum to one at each level, and they are consistent along label injections, so these laws form an exchangeable graph law L_f. By Möbius inversion its upper masses P(F ≤ ·) are the values f(F), and multiplicativity of f then says exactly that L_f is dissociated.

This is the random object behind the classical proof of representability: a dissociated exchangeable graph law is the sampling law of a graphon W, whose upper masses are the homomorphism densities t(·, W), so f = t(·, W). No graphon is involved in the construction here.

Main definitions

• TauCeti.DenseGraphLimits.paramGraphLaw — the measure on the graphs on Fin n with mass f†(H) at each H, as a weighted sum of Dirac masses;
• TauCeti.DenseGraphLimits.paramExchangeableLaw — the exchangeable graph law L_f with these level measures.

Main results

• TauCeti.DenseGraphLimits.paramGraphLaw_apply — the mass of a set of graphs is the sum of the clipped nonnegative Möbius weights of its members;
• TauCeti.DenseGraphLimits.isProbabilityMeasure_paramGraphLaw — each level is a probability measure;
• TauCeti.DenseGraphLimits.paramGraphLaw_map_comap — the levels are consistent along label injections;
• TauCeti.DenseGraphLimits.paramExchangeableLaw_upperMass — the upper masses of L_f are the values of f;
• TauCeti.DenseGraphLimits.isDissociated_paramExchangeableLaw — L_f is dissociated.

Implementation

The weights of paramGraphLaw are ENNReal.ofReal (f†(H)), so the measure is defined for every parameter; the structural conditions enter only through the theorems. Nonnegativity of f†, a consequence of isomorphism invariance and reflection positivity, is what makes these weights faithful to the real identities of the Möbius calculus, which is why reflection positivity is a hypothesis of the consistency theorem even though the underlying identity graphParamMobius_sum_comap does not need it.

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Section 2 — the random graph with probabilities f† in the proof of Theorem 2.2.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 5.3 and Chapter 11.

noncomputable def TauCeti.DenseGraphLimits.paramGraphLaw (f : GraphParam) (n : ℕ) : MeasureTheory.Measure (SimpleGraph (Fin n))

The level-n law of a graph parameter: the measure on the graphs on Fin n with mass f†(H) at each H, clipped at 0. For a parameter satisfying the structural conditions it is a probability measure (isProbabilityMeasure_paramGraphLaw).

Equations

• TauCeti.DenseGraphLimits.paramGraphLaw f n = ∑ H : SimpleGraph (Fin n), ENNReal.ofReal (TauCeti.DenseGraphLimits.graphParamMobius f n H) • MeasureTheory.Measure.dirac H

theorem TauCeti.DenseGraphLimits.paramGraphLaw_apply (f : GraphParam) (n : ℕ) (s : Set (SimpleGraph (Fin n))) : (paramGraphLaw f n) s = ∑ H : SimpleGraph (Fin n) with H ∈ s, ENNReal.ofReal (graphParamMobius f n H)

The mass of a set of graphs under paramGraphLaw is the sum of the clipped nonnegative Möbius weights of its members.

@[simp]

theorem TauCeti.DenseGraphLimits.paramGraphLaw_singleton (f : GraphParam) (n : ℕ) (H : SimpleGraph (Fin n)) : (paramGraphLaw f n) {H} = ENNReal.ofReal (graphParamMobius f n H)

The mass of a single graph under paramGraphLaw is its clipped nonnegative Möbius weight.

theorem TauCeti.DenseGraphLimits.isProbabilityMeasure_paramGraphLaw (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (paramGraphLaw f n)

For a parameter satisfying the structural conditions, each level law is a probability measure: the Möbius masses are nonnegative and sum to one.

theorem TauCeti.DenseGraphLimits.paramGraphLaw_map_comap (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) {k n : ℕ} (e : Fin k ↪ Fin n) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑e) (paramGraphLaw f n) = paramGraphLaw f k

Consistency of the level laws. For a parameter satisfying the structural conditions, restricting the level-n law along a label injection e : Fin k ↪ Fin n gives the level-k law.

noncomputable def TauCeti.DenseGraphLimits.paramExchangeableLaw (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) : ExchangeableGraphLaw

The exchangeable graph law L_f of a parameter satisfying the structural conditions: its level-n marginal gives each graph H on Fin n the Möbius mass f†(H).

Equations

• TauCeti.DenseGraphLimits.paramExchangeableLaw f hiso hmul hnorm hrp = { law := TauCeti.DenseGraphLimits.paramGraphLaw f, prob := ⋯, consistent := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.paramExchangeableLaw_law (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) (n : ℕ) : (paramExchangeableLaw f hiso hmul hnorm hrp).law n = paramGraphLaw f n

The marginals of L_f are the level laws paramGraphLaw f.

@[simp]

theorem TauCeti.DenseGraphLimits.paramExchangeableLaw_upperMass (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) {k : ℕ} (F : SimpleGraph (Fin k)) : (paramExchangeableLaw f hiso hmul hnorm hrp).upperMass F = f k F

The upper masses of L_f are the values of f. By Möbius inversion, the probability that the level-k sample contains F is ∑_{G ≥ F} f†(G) = f(F).

theorem TauCeti.DenseGraphLimits.isDissociated_paramExchangeableLaw (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (hrp : IsReflectionPositive f) : (paramExchangeableLaw f hiso hmul hnorm hrp).IsDissociated

L_f is dissociated. Its upper masses are the values of f, which are multiplicative over disjoint unions.