The Möbius transform of a graph parameter

For a graph parameter f and a graph F on Fin n, the Möbius transform f†(F) = ∑_{G ≥ F} (-1)^{e(G) - e(F)} f(G) is the coefficient of F when f, restricted to the graphs on Fin n, is expanded in the "contains exactly" basis: Möbius inversion over the Boolean lattice of graphs on Fin n says f(F) = ∑_{G ≥ F} f†(G), and f† is the only function with that property. For the homomorphism density f = t(·, W) of a graphon, f†(F) is classically the probability that the W-random graph on n vertices is exactly F; this file does not use that interpretation.

For an arbitrary parameter, the structural conditions of the Lovász–Szegedy representability theorem make f† a probability mass function at each level:

• isomorphism invariance together with reflection positivity makes it nonnegative. The connection matrix of the fully labeled graphs on Fin n has entries f(G ⊔ G'), which by inversion is Z · diag(f†) · Zᵀ for the zeta matrix Z(G, H) = [G ≤ H]. The zeta matrix is invertible, so this connection matrix is positive semidefinite exactly when every f†(H) is nonnegative;
• multiplicativity and normalization make it sum to one, since the total mass is f of the edgeless graph;
• isomorphism invariance, multiplicativity and normalization make the levels consistent: for a label injection e : Fin k ↪ Fin n, the mass f†(G) is the total mass of the graphs H on Fin n with H.comap e = G. Both sides have the same sums over the supergraphs of any F, namely f(F) and f(F.map e), and relabeling F into Fin n adjoins isolated vertices, which does not change f.

These are the facts that turn a parameter satisfying the structural conditions into a random graph model whose upper masses P(F ≤ ·) are the values of f.

Main definitions

• TauCeti.DenseGraphLimits.graphParamMobius is the Möbius transform f†.

Main results

• TauCeti.DenseGraphLimits.sum_graphParamMobius_filter_le — Möbius inversion ∑_{G ≥ F} f†(G) = f(F);
• TauCeti.DenseGraphLimits.eq_graphParamMobius_iff — f† is the unique function with that property;
• TauCeti.DenseGraphLimits.connectionMatrix_fullyLabeled — the factorization C = Z · diag(f†) · Zᵀ of the connection matrix of the fully labeled graphs on Fin n, for an isomorphism-invariant parameter;
• TauCeti.DenseGraphLimits.posSemidef_connectionMatrix_fullyLabeled_iff — that connection matrix is positive semidefinite iff the Möbius masses at level n are nonnegative;
• TauCeti.DenseGraphLimits.graphParamMobius_nonneg — f† ≥ 0 for an isomorphism-invariant, reflection-positive parameter;
• TauCeti.DenseGraphLimits.graphParamMobius_sum_eq_one — ∑ f† = 1 at every level for a multiplicative, normalized parameter;
• TauCeti.DenseGraphLimits.graphParamMobius_sum_comap — the Möbius consistency f†(G) = ∑_{H.comap e = G} f†(H) along every label injection e, for an isomorphism-invariant, multiplicative, normalized parameter.

The section Examples computes the transforms of the homomorphism densities of the constant graphons 1 and 0: point masses at the complete and at the edgeless graph.

Implementation

Edge counts are Nat.card G.edgeSet, so the transform needs no decidability of adjacency in the summed graphs. The factorization, and with it nonnegativity, assumes isomorphism invariance: the gluing of two fully labeled graphs is G ⊔ G' only up to the relabeling in LabeledGraph.glue (LabeledGraph.glueFullyLabeledIso), and invariance is what identifies its value with f(G ⊔ G'). The zeta and Möbius matrices are SimpleGraph.zetaMatrix and SimpleGraph.mobiusMatrix.

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Section 2 — the Möbius transform f† and its role in the proof of Theorem 2.2.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Sections 4.3 and 5.3.

noncomputable def TauCeti.DenseGraphLimits.graphParamMobius (f : GraphParam) : GraphParam

The Möbius transform f† of a graph parameter over supergraphs on the same vertex set: f†(F) = ∑_{G ≥ F} (-1)^{e(G) - e(F)} f(G), the coefficients of f in the "contains exactly" basis. Edge counts are Nat.card, so no decidability is needed on the summed graphs.

Equations

• TauCeti.DenseGraphLimits.graphParamMobius f n F = ∑ G : SimpleGraph (Fin n) with F ≤ G, (-1) ^ (Nat.card ↑G.edgeSet - Nat.card ↑F.edgeSet) * f n G

theorem TauCeti.DenseGraphLimits.graphParamMobius_apply (f : GraphParam) (n : ℕ) (F : SimpleGraph (Fin n)) : graphParamMobius f n F = ∑ G : SimpleGraph (Fin n) with F ≤ G, (-1) ^ (Nat.card ↑G.edgeSet - Nat.card ↑F.edgeSet) * f n G

The defining formula of the Möbius transform. This is an explicit rewrite rule rather than a simp lemma, so simplification can recognize the outer sum in sum_graphParamMobius_filter_le before unfolding its summands.

@[simp]

theorem TauCeti.DenseGraphLimits.sum_graphParamMobius_filter_le (f : GraphParam) {n : ℕ} (F : SimpleGraph (Fin n)) : ∑ G : SimpleGraph (Fin n) with F ≤ G, graphParamMobius f n G = f n F

Möbius inversion. The Möbius masses of the supergraphs of F add up to f(F): the signed sum over each interval [F, H] cancels unless F = H.

theorem TauCeti.DenseGraphLimits.eq_graphParamMobius_iff (f : GraphParam) {n : ℕ} (g : SimpleGraph (Fin n) → ℝ) : g = graphParamMobius f n ↔ ∀ (F : SimpleGraph (Fin n)), ∑ G : SimpleGraph (Fin n) with F ≤ G, g G = f n F

f† is characterized by Möbius inversion. A function g on the graphs on Fin n is the Möbius transform of f exactly when its masses on the supergraphs of every F add up to f(F).

theorem TauCeti.DenseGraphLimits.graphParamMobius_sum_eq_one (f : GraphParam) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (n : ℕ) : ∑ G : SimpleGraph (Fin n), graphParamMobius f n G = 1

The Möbius masses sum to one. For a multiplicative, normalized parameter the total mass at every level is f of the edgeless graph, which is 1.

theorem TauCeti.DenseGraphLimits.graphParamMobius_sum_comap (f : GraphParam) (hiso : IsIsoInvariant f) (hmul : IsMultiplicative f) (hnorm : IsNormalized f) {k n : ℕ} (e : Fin k ↪ Fin n) (G : SimpleGraph (Fin k)) : graphParamMobius f k G = ∑ H : SimpleGraph (Fin n) with SimpleGraph.comap (⇑e) H = G, graphParamMobius f n H

Möbius consistency. For an isomorphism-invariant, multiplicative, normalized parameter, the Möbius mass of a graph G on Fin k is the total Möbius mass of the graphs on Fin n whose restriction along the label injection e is G. Reflection positivity is not needed.

theorem TauCeti.DenseGraphLimits.connectionMatrix_fullyLabeled (f : GraphParam) (hf : IsIsoInvariant f) (n : ℕ) : connectionMatrix f LabeledGraph.fullyLabeled = SimpleGraph.zetaMatrix (Fin n) ℝ * Matrix.diagonal (graphParamMobius f n) * (SimpleGraph.zetaMatrix (Fin n) ℝ).transpose

The connection-matrix factorization C = Z · diag(f†) · Zᵀ. For an isomorphism-invariant parameter, the connection matrix of the fully labeled graphs on Fin n has entries f(G ⊔ G'), and Möbius inversion expands them as ∑_H [G ≤ H] [G' ≤ H] f†(H): the connection matrix is the congruence of the diagonal matrix of Möbius masses by the zeta matrix of the lattice of graphs.

theorem TauCeti.DenseGraphLimits.posSemidef_connectionMatrix_fullyLabeled_iff (f : GraphParam) (hf : IsIsoInvariant f) (n : ℕ) : (connectionMatrix f LabeledGraph.fullyLabeled).PosSemidef ↔ ∀ (H : SimpleGraph (Fin n)), 0 ≤ graphParamMobius f n H

Reflection positivity on the fully labeled graphs is nonnegativity of the Möbius masses. For an isomorphism-invariant parameter, the connection matrix of the fully labeled graphs on Fin n is positive semidefinite exactly when every Möbius mass f†(H) of a graph on Fin n is nonnegative: by connectionMatrix_fullyLabeled it is congruent to the diagonal matrix of Möbius masses, and the zeta matrix is invertible.

theorem TauCeti.DenseGraphLimits.graphParamMobius_nonneg (f : GraphParam) (hiso : IsIsoInvariant f) (hrp : IsReflectionPositive f) (n : ℕ) (F : SimpleGraph (Fin n)) : 0 ≤ graphParamMobius f n F

Isomorphism invariance and reflection positivity make the Möbius masses nonnegative: the connection matrix of the fully labeled graphs on Fin n is positive semidefinite, which by posSemidef_connectionMatrix_fullyLabeled_iff is the nonnegativity of the Möbius masses.

The constant graphons

The homomorphism density of the constant graphon 1 is the parameter constantly 1; that of the constant graphon 0 is 1 on the edgeless graphs and 0 otherwise. Their Möbius transforms are the point masses at the complete and at the edgeless graph: the 1-random graph is complete, and the 0-random graph is edgeless.