Edge-supported positive part and the Gram form

If X is symmetric then B = A_G ⊙ X₊ is symmetric, entrywise nonnegative, zero-diagonal, and supported on the edges of G. Pairing against X or B gives the same Frobenius mass. Combined with the weighted Motzkin–Straus bound and the rank-two variational lemma, this yields thm:gram.

BollobasNikiforov.Spectral.Variational cannot be imported here: it shares inner_vecMulVec with BollobasNikiforov.MS.Basic (pulled in by Weighted), and also overlaps Weighted on inner_smul_vecMulVec, inner_vecMulVec_vecMulVec, and eigenvectorBasis_dotProduct. The CG03 argument is therefore reproduced in GramAux.

CG03, locally, to avoid import clashes with Weighted

theorem BollobasNikiforov.GramAux.eigenvectorBasis_dotProduct_self {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (i : n) : (hB.eigenvectorBasis i).ofLp ⬝ᵥ (hB.eigenvectorBasis i).ofLp = 1

theorem BollobasNikiforov.GramAux.eigenvectorBasis_dotProduct {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) {i j : n} (hij : i ≠ j) : (hB.eigenvectorBasis i).ofLp ⬝ᵥ (hB.eigenvectorBasis j).ofLp = 0

theorem BollobasNikiforov.GramAux.parseval_eigenvectorBasis {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (x : n → ℝ) : ∑ k : n, ((hB.eigenvectorBasis k).ofLp ⬝ᵥ x) ^ 2 = x ⬝ᵥ x

theorem BollobasNikiforov.GramAux.vecMulVec_mulVec_real {n : Type u_1} [Fintype n] (u v x : n → ℝ) : (Matrix.vecMulVec u v).mulVec x = (v ⬝ᵥ x) • u

theorem BollobasNikiforov.GramAux.isHermitian_quadratic {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) (x : n → ℝ) : x ⬝ᵥ B.mulVec x = ∑ k : n, hB.eigenvalues k * ((hB.eigenvectorBasis k).ofLp ⬝ᵥ x) ^ 2

theorem BollobasNikiforov.GramAux.eigenvalues_le_lambdaMax {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nonempty n] (hB : B.IsHermitian) (i : n) : hB.eigenvalues i ≤ lambdaMax hB

theorem BollobasNikiforov.GramAux.rayleigh_le_lambdaMax {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nonempty n] (hB : B.IsHermitian) {u : n → ℝ} (hu : u ⬝ᵥ u = 1) : u ⬝ᵥ B.mulVec u ≤ lambdaMax hB

theorem BollobasNikiforov.GramAux.exists_rankTwo_writing {n : Type u_1} [Fintype n] [Nontrivial n] {X : Matrix n n ℝ} (hX : X.PosSemidef) (hr : X.rank ≤ 2) : ∃ (u : n → ℝ) (v : n → ℝ) (α : ℝ) (β : ℝ), 0 ≤ β ∧ β ≤ α ∧ u ⬝ᵥ u = 1 ∧ v ⬝ᵥ v = 1 ∧ u ⬝ᵥ v = 0 ∧ X = α • Matrix.vecMulVec u u + β • Matrix.vecMulVec v v

theorem BollobasNikiforov.GramAux.bessel_two {n : Type u_1} [Fintype n] {u v x : n → ℝ} (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0) : (u ⬝ᵥ x) ^ 2 + (v ⬝ᵥ x) ^ 2 ≤ x ⬝ᵥ x

theorem BollobasNikiforov.GramAux.sum_antitone_le_two_largest {m : ℕ} (hm : 2 ≤ m) (lam q : Fin m → ℝ) (hlam : Antitone lam) (hq0 : ∀ (i : Fin m), 0 ≤ q i) (hq1 : ∀ (i : Fin m), q i ≤ 1) (hsum : ∑ i : Fin m, q i = 2) : ∑ i : Fin m, lam i * q i ≤ lam ⟨0, ⋯⟩ + lam ⟨1, ⋯⟩

theorem BollobasNikiforov.GramAux.orthonormal_pair_le_lambdaMax_add_lambdaSecond {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} [Nontrivial n] (hB : B.IsHermitian) {u v : n → ℝ} (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0) : u ⬝ᵥ B.mulVec u + v ⬝ᵥ B.mulVec v ≤ lambdaMax hB + lambdaSecond hB

theorem BollobasNikiforov.GramAux.inner_vecMulVec' {n : Type u_1} [Fintype n] (C : Matrix n n ℝ) (u : n → ℝ) : inner C (Matrix.vecMulVec u u) = u ⬝ᵥ C.mulVec u

theorem BollobasNikiforov.GramAux.inner_smul_vecMulVec' {n : Type u_1} [Fintype n] (r : ℝ) (C : Matrix n n ℝ) (u : n → ℝ) : inner C (r • Matrix.vecMulVec u u) = r * u ⬝ᵥ C.mulVec u

theorem BollobasNikiforov.GramAux.inner_vecMulVec_vecMulVec' {n : Type u_1} [Fintype n] (u v : n → ℝ) : inner (Matrix.vecMulVec u u) (Matrix.vecMulVec v v) = (u ⬝ᵥ v) ^ 2

theorem BollobasNikiforov.GramAux.inner_rankTwo {n : Type u_1} [Fintype n] (C : Matrix n n ℝ) (u v : n → ℝ) (α β : ℝ) : inner C (α • Matrix.vecMulVec u u + β • Matrix.vecMulVec v v) = α * u ⬝ᵥ C.mulVec u + β * v ⬝ᵥ C.mulVec v

theorem BollobasNikiforov.GramAux.inner_self_rankTwo {n : Type u_1} [Fintype n] {u v : n → ℝ} (hu : u ⬝ᵥ u = 1) (hv : v ⬝ᵥ v = 1) (huv : u ⬝ᵥ v = 0) (α β : ℝ) : inner (α • Matrix.vecMulVec u u + β • Matrix.vecMulVec v v) (α • Matrix.vecMulVec u u + β • Matrix.vecMulVec v v) = α ^ 2 + β ^ 2

theorem BollobasNikiforov.GramAux.cauchySchwarz_two (α β a b : ℝ) : α * a + β * b ≤ √(α ^ 2 + β ^ 2) * √(a ^ 2 + b ^ 2)

theorem BollobasNikiforov.GramAux.exists_card_one_writing {n : Type u_1} [Fintype n] (hn : Fintype.card n = 1) {X : Matrix n n ℝ} (hX : X.PosSemidef) : ∃ (u : n → ℝ) (α : ℝ), 0 ≤ α ∧ u ⬝ᵥ u = 1 ∧ X = α • Matrix.vecMulVec u u

theorem BollobasNikiforov.GramAux.variational_lemma {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.IsHermitian) {X : Matrix n n ℝ} (hX : X.PosSemidef) (hr : X.rank ≤ 2) : inner B X ≤ √(F hB) * √(inner X X)

Local copy of CG03 (lem:variational).

theorem BollobasNikiforov.max_zero_mul_self (x : ℝ) : max x 0 * x = max x 0 ^ 2

max x 0 * x = (max x 0)².

theorem BollobasNikiforov.posPart_isSymm {V : Type u_1} {X : Matrix V V ℝ} (hX : X.IsSymm) : (posPart X).IsSymm

theorem BollobasNikiforov.isSymm_adjMatrix_hadamard_posPart {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hX : X.IsSymm) : ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)).IsSymm

CG04. A_G ⊙ X₊ is symmetric when X is.

theorem BollobasNikiforov.adjMatrix_hadamard_posPart_nonneg {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] (X : Matrix V V ℝ) (i j : V) : 0 ≤ (SimpleGraph.adjMatrix ℝ G).hadamard (posPart X) i j

CG04. A_G ⊙ X₊ is entrywise nonnegative.

theorem BollobasNikiforov.adjMatrix_hadamard_posPart_diag {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] (X : Matrix V V ℝ) (i : V) : (SimpleGraph.adjMatrix ℝ G).hadamard (posPart X) i i = 0

CG04. A_G ⊙ X₊ has zero diagonal.

theorem BollobasNikiforov.adjMatrix_hadamard_posPart_eq_zero_of_not_adj {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} {i j : V} (hij : ¬G.Adj i j) : (SimpleGraph.adjMatrix ℝ G).hadamard (posPart X) i j = 0

CG04. A_G ⊙ X₊ vanishes off the edges of G.

theorem BollobasNikiforov.inner_adjMatrix_hadamard_posPart {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] (X : Matrix V V ℝ) : inner ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)) X = inner ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)) ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X))

CG04. On this support, ⟨B, X⟩ = ⟨B, B⟩.

theorem BollobasNikiforov.inner_adjMatrix_hadamard_posPart_self {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] (X : Matrix V V ℝ) : inner ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)) ((SimpleGraph.adjMatrix ℝ G).hadamard (posPart X)) = ∑ i : V, ∑ j : V, SimpleGraph.adjMatrix ℝ G i j * posPart X i j ^ 2

Adjacency entries are 0-1, so A ⊙ X₊ has the same Frobenius mass as the weighted sum of squared positive parts.

theorem BollobasNikiforov.gram_le {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] {X : Matrix V V ℝ} (hX : X.PosSemidef) (hr : X.rank ≤ 2) : ∑ i : V, ∑ j : V, SimpleGraph.adjMatrix ℝ G i j * posPart X i j ^ 2 ≤ turanFactor G * inner X X

CG05. Theorem thm:gram. Named gram_le because BollobasNikiforov.gram is already the planar Gram matrix in BollobasNikiforov.M.HalfPlane.