Motzkin–Straus

The Motzkin–Straus theorem bounds the adjacency quadratic form on the nonnegative orthant by the Turán factor 1 - 1/ω(G), and the same bound passes to the Frobenius pairing against a completely positive matrix.

The standard simplex

Mathlib's set-valued stdSimplex was deprecated in favour of the bundled type Convexity.StdSimplex. The Motzkin–Straus argument below perturbs a vector inside the simplex and compares it against the ambient quadratic form, so it works with the set of vectors rather than with a bundled carrier.

def BollobasNikiforov.stdSimplex (𝕜 : Type u_2) [AddCommMonoid 𝕜] [PartialOrder 𝕜] [One 𝕜] (ι : Type u_3) [Fintype ι] : Set (ι → 𝕜)

The standard simplex in ι → 𝕜: the vectors with nonnegative coordinates summing to 1.

Equations

• BollobasNikiforov.stdSimplex 𝕜 ι = {f : ι → 𝕜 | (∀ (i : ι), 0 ≤ f i) ∧ ∑ i : ι, f i = 1}

theorem BollobasNikiforov.single_mem_stdSimplex {ι : Type u_2} [Fintype ι] [DecidableEq ι] (i : ι) : Pi.single i 1 ∈ stdSimplex ℝ ι

Each vertex Pi.single i 1 lies in the standard simplex.

theorem BollobasNikiforov.stdSimplex_subset_Icc (ι : Type u_2) [Fintype ι] : stdSimplex ℝ ι ⊆ Set.Icc 0 1

Every coordinate of a point of the standard simplex lies in [0, 1].

theorem BollobasNikiforov.isClosed_stdSimplex (ι : Type u_2) [Fintype ι] : IsClosed (stdSimplex ℝ ι)

theorem BollobasNikiforov.isCompact_stdSimplex (ι : Type u_2) [Fintype ι] : IsCompact (stdSimplex ℝ ι)

The standard simplex is compact: it is a closed subset of the unit cube.

MS05 — Cauchy–Schwarz on a block of size k

theorem BollobasNikiforov.sum_sq_le_card_mul_sum_sq_finset {ι : Type u_2} (s : Finset ι) (y : ι → ℝ) : (∑ i ∈ s, y i) ^ 2 ≤ ↑s.card * ∑ i ∈ s, y i ^ 2

theorem BollobasNikiforov.sum_sq_le_card_mul_sum_sq {ι : Type u_2} [Fintype ι] (y : ι → ℝ) : (∑ i : ι, y i) ^ 2 ≤ ↑(Fintype.card ι) * ∑ i : ι, y i ^ 2

MS05. Cauchy–Schwarz against the all-ones vector: (∑ y)² ≤ k ∑ yᵢ².

theorem BollobasNikiforov.sum_sq_sub_sum_sq_le_finset {ι : Type u_2} (s : Finset ι) (y : ι → ℝ) (hk : 1 ≤ s.card) : (∑ i ∈ s, y i) ^ 2 - ∑ i ∈ s, y i ^ 2 ≤ (1 - 1 / ↑s.card) * (∑ i ∈ s, y i) ^ 2

theorem BollobasNikiforov.sum_sq_sub_sum_sq_le {ι : Type u_2} [Fintype ι] (y : ι → ℝ) (hk : 1 ≤ Fintype.card ι) : (∑ i : ι, y i) ^ 2 - ∑ i : ι, y i ^ 2 ≤ (1 - 1 / ↑(Fintype.card ι)) * (∑ i : ι, y i) ^ 2

MS05. If k ≥ 1 then (∑ y)² - ∑ y² ≤ (1 - 1/k) (∑ y)².

MS01 — quadratic form as an edge sum

theorem BollobasNikiforov.mulVec_adjMatrix_dotProduct {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (y : V → ℝ) : (SimpleGraph.adjMatrix ℝ G).mulVec y ⬝ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then y i * y j else 0

MS01. The adjacency quadratic form expands as a sum over edges.

theorem BollobasNikiforov.continuous_adjMatrix_quadratic {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] : Continuous fun (y : V → ℝ) => y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y

MS02 — affinity along a nonedge

theorem BollobasNikiforov.add_smul_e_sub_e_apply {V : Type u_1} [DecidableEq V] {i j : V} (hne : i ≠ j) (y : V → ℝ) (t : ℝ) (k : V) : (y + t • (e i - e j)) k = if k = i then y i + t else if k = j then y j - t else y k

theorem BollobasNikiforov.sum_e_sub_e {V : Type u_1} [Fintype V] [DecidableEq V] {i j : V} : ∑ k : V, (e i - e j) k = 0

theorem BollobasNikiforov.add_smul_e_sub_e_mem_stdSimplex {V : Type u_1} [Fintype V] [DecidableEq V] {i j : V} (hne : i ≠ j) {y : V → ℝ} (hy : y ∈ stdSimplex ℝ V) {t : ℝ} (hti : 0 ≤ y i + t) (htj : 0 ≤ y j - t) : y + t • (e i - e j) ∈ stdSimplex ℝ V

theorem BollobasNikiforov.adjMatrix_quadratic_e_sub_e {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {i j : V} (hij : ¬G.Adj i j) (_hne : i ≠ j) : (e i - e j) ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec (e i - e j) = 0

The second-difference coefficient along a nonedge vanishes: Aᵢᵢ = Aⱼⱼ = Aᵢⱼ = 0.

theorem BollobasNikiforov.adjMatrix_dotProduct_e_sub_e {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (y : V → ℝ) {i j : V} : (e i - e j) ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y = (SimpleGraph.adjMatrix ℝ G).mulVec y i - (SimpleGraph.adjMatrix ℝ G).mulVec y j

theorem BollobasNikiforov.adjMatrix_quadratic_symm {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (y d : V → ℝ) : y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec d = d ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y

theorem BollobasNikiforov.adjMatrix_quadratic_add_smul_single_sub_single {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {i j : V} (hij : ¬G.Adj i j) (hne : i ≠ j) (y : V → ℝ) (t : ℝ) (hti : 0 ≤ y i + t) (htj : 0 ≤ y j - t) : (y + t • (e i - e j)) ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec (y + t • (e i - e j)) = y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y + 2 * t * ((SimpleGraph.adjMatrix ℝ G).mulVec y i - (SimpleGraph.adjMatrix ℝ G).mulVec y j)

MS02. Along a nonedge the adjacency quadratic is affine in the transfer parameter t. The inequalities keep the perturbation nonnegative and are used in MS03.

MS03 — a maximizer with clique support

theorem BollobasNikiforov.stdSimplex_nonempty {V : Type u_1} [Fintype V] [Nonempty V] : (stdSimplex ℝ V).Nonempty

theorem BollobasNikiforov.exists_isMaxOn_adjMatrix_quadratic {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : ∃ y ∈ stdSimplex ℝ V, IsMaxOn (fun (y : V → ℝ) => y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y) (stdSimplex ℝ V) y

theorem BollobasNikiforov.exists_isMaxOn_adjMatrix_quadratic_isClique_support {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : ∃ y ∈ stdSimplex ℝ V, IsMaxOn (fun (y : V → ℝ) => y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y) (stdSimplex ℝ V) y ∧ G.IsClique {v : V | y v ≠ 0}

MS03. The adjacency quadratic attains its maximum on the simplex, and some maximizer is supported on a clique.

MS04 — clique computation

theorem BollobasNikiforov.adjMatrix_quadratic_eq_sum_sq_sub_of_isClique {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {s : Set V} (hs : G.IsClique s) {y : V → ℝ} (hsupp : ∀ (v : V), y v ≠ 0 → v ∈ s) : y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y = (∑ i : V, y i) ^ 2 - ∑ i : V, y i ^ 2

MS04. On a clique the adjacency quadratic is (∑ y)² - ∑ y².

MS06 — Motzkin–Straus

theorem BollobasNikiforov.adjMatrix_quadratic_le_turanFactor_of_isClique_support {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {y : V → ℝ} (hy : y ∈ stdSimplex ℝ V) (hc : G.IsClique {v : V | y v ≠ 0}) : y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y ≤ turanFactor G

theorem BollobasNikiforov.adjMatrix_quadratic_le_turanFactor_of_mem_stdSimplex {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] {y : V → ℝ} (hy : y ∈ stdSimplex ℝ V) : y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y ≤ turanFactor G

theorem BollobasNikiforov.adjMatrix_quadratic_smul {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (c : ℝ) (y : V → ℝ) : c • y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec (c • y) = c ^ 2 * y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y

theorem BollobasNikiforov.motzkinStraus {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {y : V → ℝ} (hy : ∀ (i : V), 0 ≤ y i) : y ⬝ᵥ (SimpleGraph.adjMatrix ℝ G).mulVec y ≤ turanFactor G * (∑ i : V, y i) ^ 2

MS06. Motzkin–Straus: yᵀ A_G y ≤ (1 - 1/ω(G)) (1ᵀ y)² for y ≥ 0.

MS07 — completely positive Motzkin–Straus

theorem BollobasNikiforov.inner_sum {V : Type u_1} [Fintype V] {ι : Type u_2} (s : Finset ι) (B : Matrix V V ℝ) (C : ι → Matrix V V ℝ) : inner B (∑ a ∈ s, C a) = ∑ a ∈ s, inner B (C a)

theorem BollobasNikiforov.inner_vecMulVec {V : Type u_1} [Fintype V] (B : Matrix V V ℝ) (p : V → ℝ) : inner B (Matrix.vecMulVec p p) = p ⬝ᵥ B.mulVec p

theorem BollobasNikiforov.inner_one_vecMulVec {V : Type u_1} [Fintype V] (p : V → ℝ) : inner (Matrix.of fun (x x_1 : V) => 1) (Matrix.vecMulVec p p) = (∑ i : V, p i) ^ 2

theorem BollobasNikiforov.inner_adjMatrix_le_turanFactor_inner {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {C : Matrix V V ℝ} (hC : IsCompletelyPositive C) : inner (SimpleGraph.adjMatrix ℝ G) C ≤ turanFactor G * inner (Matrix.of fun (x x_1 : V) => 1) C

MS07. Completely positive Motzkin–Straus: ⟨A_G, C⟩ ≤ (1 - 1/ω(G)) ⟨J, C⟩ for C completely positive.