Graph parameters, connection matrices and reflection positivity

A graph parameter assigns a real number to every finite simple graph. Its connection matrices are the matrices of its values on the gluings of a finite family of k-labeled graphs; a parameter is reflection positive when all of them are positive semidefinite. Together with multiplicativity over disjoint unions and normalization at the one-vertex graph, these are the structural conditions of the Lovász–Szegedy representability theorem.

Main definitions

• TauCeti.DenseGraphLimits.GraphParam is a real parameter of finite simple graphs, with TauCeti.DenseGraphLimits.IsIsoInvariant imposing agreement along isomorphisms;
• TauCeti.DenseGraphLimits.connectionMatrix is an indexed block of the connection matrix M(f, k);
• TauCeti.DenseGraphLimits.IsReflectionPositive, TauCeti.DenseGraphLimits.IsMultiplicative and TauCeti.DenseGraphLimits.IsNormalized are the three remaining structural conditions.

Main results

• TauCeti.DenseGraphLimits.isIsoInvariant_iff, TauCeti.DenseGraphLimits.isReflectionPositive_iff, TauCeti.DenseGraphLimits.isMultiplicative_iff and TauCeti.DenseGraphLimits.isNormalized_iff are the characteristic laws of the four structural conditions, by which each of them is both established and applied;
• TauCeti.DenseGraphLimits.isHermitian_connectionMatrix — isomorphism invariance makes connection matrices Hermitian because the two gluing orders are isomorphic;
• TauCeti.DenseGraphLimits.IsReflectionPositive.posSemidef reindexes the definition, which quantifies over Fin n-indexed families, to an arbitrary finite index type;
• TauCeti.DenseGraphLimits.IsReflectionPositive.nonneg_glue_self is the diagonal consequence 0 ≤ f on a self-gluing;
• TauCeti.DenseGraphLimits.IsMultiplicative.apply_sum_bot says adjoining any finite edgeless graph does not change a multiplicative, normalized parameter, and TauCeti.DenseGraphLimits.IsMultiplicative.apply_map that neither does relabeling a graph into a larger vertex set along an injection, when the parameter is also isomorphism invariant.

The section Examples records that the four conditions are simultaneously satisfiable — the parameter constantly 1, which is the homomorphism density of the constant graphon W ≡ 1 — and that reflection positivity is not automatic.

Implementation

connectionMatrix takes an arbitrary index type: the Matrix ι ι ℝ it produces needs no finiteness, and IsReflectionPositive supplies Fin n where positive semidefiniteness is asserted. IsReflectionPositive.posSemidef then recovers the arbitrary finite index case, since a connection matrix on ι is a submatrix of one on Fin (Fintype.card ι) along Fintype.equivFin.

References

• L. Lovász, B. Szegedy, Limits of dense graph sequences, JCTB 96 (2006), 933–957, Theorem 2.2 — the four structural conditions and the representability theorem they characterise.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Chapters 5 and 6.

@[reducible, inline]

abbrev TauCeti.DenseGraphLimits.GraphParam : Type

A graph parameter: a real-valued parameter of finite simple graphs, indexed over the Fin-representatives. Isomorphism invariance is imposed separately, as IsIsoInvariant.

Equations

• TauCeti.DenseGraphLimits.GraphParam = ((n : ℕ) → SimpleGraph (Fin n) → ℝ)

def TauCeti.DenseGraphLimits.IsIsoInvariant (f : GraphParam) : Prop

A graph parameter is isomorphism invariant when it agrees on isomorphic graphs. This is the standing hypothesis that makes f a genuine parameter of graphs rather than a labelling-sensitive function on Fin n.

Equations

• TauCeti.DenseGraphLimits.IsIsoInvariant f = ∀ (n₁ n₂ : ℕ) (F₁ : SimpleGraph (Fin n₁)) (F₂ : SimpleGraph (Fin n₂)), Nonempty (F₁ ≃g F₂) → f n₁ F₁ = f n₂ F₂

theorem TauCeti.DenseGraphLimits.isIsoInvariant_iff {f : GraphParam} : IsIsoInvariant f ↔ ∀ (n₁ n₂ : ℕ) (F₁ : SimpleGraph (Fin n₁)) (F₂ : SimpleGraph (Fin n₂)), Nonempty (F₁ ≃g F₂) → f n₁ F₁ = f n₂ F₂

Characteristic law of isomorphism invariance: f is isomorphism invariant exactly when it takes equal values at any two isomorphic graphs. This is both the way to prove IsIsoInvariant and the way to apply it.

theorem TauCeti.DenseGraphLimits.IsIsoInvariant.eq_of_iso {f : GraphParam} (hf : IsIsoInvariant f) {n₁ n₂ : ℕ} {F₁ : SimpleGraph (Fin n₁)} {F₂ : SimpleGraph (Fin n₂)} (e : F₁ ≃g F₂) : f n₁ F₁ = f n₂ F₂

An isomorphism-invariant parameter agrees along an isomorphism.

noncomputable def TauCeti.DenseGraphLimits.connectionMatrix (f : GraphParam) {k : ℕ} {ι : Type u_1} (A : ι → LabeledGraph k) : Matrix ι ι ℝ

The connection matrix of a graph parameter on a family A : ι → LabeledGraph k of k-labeled graphs: the ι × ι matrix whose (i, j) entry is f on the unlabeled graph underlying the gluing of A i and A j. It is an indexed block of the full connection matrix M(f, k).

Equations

• TauCeti.DenseGraphLimits.connectionMatrix f A = Matrix.of fun (i j : ι) => f ((A i).glue (A j)).forgetLabels.fst ((A i).glue (A j)).forgetLabels.snd

@[simp]

theorem TauCeti.DenseGraphLimits.connectionMatrix_apply (f : GraphParam) {k : ℕ} {ι : Type u_1} (A : ι → LabeledGraph k) (i j : ι) : connectionMatrix f A i j = f ((A i).glue (A j)).forgetLabels.fst ((A i).glue (A j)).forgetLabels.snd

The connection-matrix entry law.

theorem TauCeti.DenseGraphLimits.connectionMatrix_comm (f : GraphParam) (hf : IsIsoInvariant f) {k : ℕ} {ι : Type u_1} (A : ι → LabeledGraph k) (i j : ι) : connectionMatrix f A i j = connectionMatrix f A j i

Connection matrices of an isomorphism-invariant parameter are symmetric: gluing commutes up to isomorphism.

theorem TauCeti.DenseGraphLimits.isHermitian_connectionMatrix (f : GraphParam) (hf : IsIsoInvariant f) {k : ℕ} {ι : Type u_1} (A : ι → LabeledGraph k) : (connectionMatrix f A).IsHermitian

Connection matrices of an isomorphism-invariant parameter are Hermitian because the two gluing orders are isomorphic.

def TauCeti.DenseGraphLimits.IsReflectionPositive (f : GraphParam) : Prop

A graph parameter is reflection positive when every finite connection matrix is positive semidefinite — every finite principal block of each M(f, k) is PSD. The definition quantifies over Fin n-indexed families; IsReflectionPositive.posSemidef recovers an arbitrary finite index type.

Equations

• TauCeti.DenseGraphLimits.IsReflectionPositive f = ∀ (k n : ℕ) (A : Fin n → TauCeti.DenseGraphLimits.LabeledGraph k), (TauCeti.DenseGraphLimits.connectionMatrix f A).PosSemidef

theorem TauCeti.DenseGraphLimits.isReflectionPositive_iff {f : GraphParam} : IsReflectionPositive f ↔ ∀ (k n : ℕ) (A : Fin n → LabeledGraph k), (connectionMatrix f A).PosSemidef

Characteristic law of reflection positivity: f is reflection positive exactly when the connection matrix of every Fin n-indexed family of k-labeled graphs is positive semidefinite. This is both the way to prove IsReflectionPositive and the way to apply it.

def TauCeti.DenseGraphLimits.IsMultiplicative (f : GraphParam) : Prop

A graph parameter is multiplicative when it turns disjoint unions into products, with the disjoint union reindexed to Fin (n₁ + n₂) along finSumFinEquiv to stay on Fin-representatives.

Equations

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

theorem TauCeti.DenseGraphLimits.isMultiplicative_iff {f : GraphParam} : IsMultiplicative f ↔ ∀ (n₁ n₂ : ℕ) (F₁ : SimpleGraph (Fin n₁)) (F₂ : SimpleGraph (Fin n₂)), f (n₁ + n₂) (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F₁ ⊕g F₂)) = f n₁ F₁ * f n₂ F₂

Characteristic law of multiplicativity: f is multiplicative exactly when it sends every reindexed disjoint union to the product of the two values. This is both the way to prove IsMultiplicative and the way to apply it.

def TauCeti.DenseGraphLimits.IsNormalized (f : GraphParam) : Prop

A graph parameter is normalized when its value on the one-vertex graph K₁ is 1.

Equations

• TauCeti.DenseGraphLimits.IsNormalized f = (f 1 ⊥ = 1)

theorem TauCeti.DenseGraphLimits.isNormalized_iff {f : GraphParam} : IsNormalized f ↔ f 1 ⊥ = 1

Characteristic law of normalization: f is normalized exactly when its value at the one-vertex graph K₁ is 1. This is both the way to prove IsNormalized and the way to apply it.

theorem TauCeti.DenseGraphLimits.IsReflectionPositive.posSemidef {f : GraphParam} (hf : IsReflectionPositive f) {k : ℕ} {ι : Type u_1} [Finite ι] (A : ι → LabeledGraph k) : (connectionMatrix f A).PosSemidef

Reflection positivity for an arbitrary finite index type. A connection matrix on ι is the Fintype.equivFin ι submatrix of one on Fin (Fintype.card ι), and positive semidefiniteness is invariant under reindexing by an equivalence.

theorem TauCeti.DenseGraphLimits.IsReflectionPositive.nonneg_glue_self {f : GraphParam} (hf : IsReflectionPositive f) {k : ℕ} (G : LabeledGraph k) : 0 ≤ f (G.glue G).n (G.glue G).graph

The diagonal of a connection matrix is nonnegative: a reflection-positive parameter is nonnegative on every self-gluing.

theorem TauCeti.DenseGraphLimits.IsMultiplicative.apply_bot {f : GraphParam} (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (n : ℕ) : f n ⊥ = 1

A multiplicative, normalized parameter is 1 on every edgeless graph.

theorem TauCeti.DenseGraphLimits.IsMultiplicative.apply_sum_bot {f : GraphParam} (hmul : IsMultiplicative f) (hnorm : IsNormalized f) (n m : ℕ) (F : SimpleGraph (Fin n)) : f (n + m) (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F ⊕g ⊥)) = f n F

A multiplicative, normalized parameter is unchanged by adjoining any finite edgeless graph.

theorem TauCeti.DenseGraphLimits.IsMultiplicative.apply_map {f : GraphParam} (hmul : IsMultiplicative f) (hiso : IsIsoInvariant f) (hnorm : IsNormalized f) {k n : ℕ} (e : Fin k ↪ Fin n) (F : SimpleGraph (Fin k)) : f n (SimpleGraph.map (⇑e) F) = f k F

An isomorphism-invariant, multiplicative, normalized parameter is unchanged by relabeling a graph into a larger vertex set along an injection: the relabeled graph is the disjoint union of the original with the edgeless graph on the vertices outside the image.

Consistency and adversarial checks

The four structural conditions are simultaneously satisfiable. Reflection positivity is not implied by isomorphism invariance alone. The parameter constantly 1 is the homomorphism density t(·, W) of the constant graphon W ≡ 1.

theorem TauCeti.DenseGraphLimits.isIsoInvariant_one : IsIsoInvariant fun (x : ℕ) (x_1 : SimpleGraph (Fin x)) => 1

The constant parameter 1 is isomorphism invariant.

theorem TauCeti.DenseGraphLimits.isMultiplicative_one : IsMultiplicative fun (x : ℕ) (x_1 : SimpleGraph (Fin x)) => 1

The constant parameter 1 is multiplicative.

theorem TauCeti.DenseGraphLimits.isNormalized_one : IsNormalized fun (x : ℕ) (x_1 : SimpleGraph (Fin x)) => 1

The constant parameter 1 is normalized.

theorem TauCeti.DenseGraphLimits.isReflectionPositive_one : IsReflectionPositive fun (x : ℕ) (x_1 : SimpleGraph (Fin x)) => 1

The constant parameter 1 is reflection positive: its connection matrices are the all-ones matrices, the outer square of the all-ones vector.

theorem TauCeti.DenseGraphLimits.not_isReflectionPositive_neg_one : ¬IsReflectionPositive fun (x : ℕ) (x_1 : SimpleGraph (Fin x)) => -1

Isomorphism invariance alone does not imply reflection positivity: the constant parameter -1 is isomorphism invariant, yet it is negative on a self-gluing.