Documentation

LeanPool.BollobasNikiforov.M.Basic

The matrix M(X) of eq:matrix #

For a real matrix X, M X = X ⊙ X + ∑_{i<j} (if X i j < 0 then (X i j)² else 0) • vecMulVec (e i - e j) (e i - e j). When X is positive semidefinite this is PSD and entrywise nonnegative.

MX01 — definition of M #

source
noncomputable def BollobasNikiforov.laplacianCoeff {n : Type u_1} [LinearOrder n] (X : Matrix n n ℝ) (i j : n) :
ℝ

The correction weight on the pair {i,j}: (X i j)² when i < j and the entry is negative, and 0 otherwise.

Equations
Instances For
    source
    noncomputable def BollobasNikiforov.M {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) :
    Matrix n n ℝ

    The map of docs/sol.tex (eq:matrix).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def BollobasNikiforov.ones {n : Type u_1} :
      Matrix n n ℝ

      The all-ones matrix, used as the Frobenius partner of M.

      Equations
      Instances For
        source
        theorem BollobasNikiforov.laplacianCoeff_nonneg {n : Type u_1} [LinearOrder n] (X : Matrix n n ℝ) (i j : n) :
        0 ≤ laplacianCoeff X i j
        source
        theorem BollobasNikiforov.M_apply {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) (a b : n) :
        M X a b = X a b * X a b + ∑ i : n, ∑ j : n, laplacianCoeff X i j * Matrix.vecMulVec (e i - e j) (e i - e j) a b

        Helpers for the rank-one Laplacian #

        source
        theorem BollobasNikiforov.vecMulVec_sub_single_offDiag {n : Type u_1} [DecidableEq n] {p q i j : n} (hij : i ≠ j) :
        Matrix.vecMulVec (e p - e q) (e p - e q) i j = if p = i ∧ q = j then -1 else if p = j ∧ q = i then -1 else 0

        Off-diagonal entries of vecMulVec (e p - e q) (e p - e q).

        source
        theorem BollobasNikiforov.sum_sum_ite_eq_pair {n : Type u_1} [Fintype n] [DecidableEq n] (f : n → n → ℝ) (i j : n) :
        (∑ p : n, ∑ q : n, if p = i ∧ q = j then f p q else 0) = f i j
        source
        theorem BollobasNikiforov.laplacianCoeff_correction_offDiag {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) {i j : n} (hij : i ≠ j) :
        ∑ p : n, ∑ q : n, laplacianCoeff X p q * Matrix.vecMulVec (e p - e q) (e p - e q) i j = -laplacianCoeff X i j - laplacianCoeff X j i

        MX03 — off-diagonal formula #

        source
        theorem BollobasNikiforov.M_apply_of_ne {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) (hX : X.IsSymm) {i j : n} (hij : i ≠ j) :
        M X i j = posPart X i j ^ 2

        For i ≠ j and symmetric X, M X i j = (max (X i j) 0)².

        MX02 — PSD and entrywise nonnegativity #

        source
        theorem BollobasNikiforov.M_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {X : Matrix n n ℝ} (hX : X.PosSemidef) :
        (M X).PosSemidef
        source
        theorem BollobasNikiforov.M_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {X : Matrix n n ℝ} (hX : X.PosSemidef) (i j : n) :
        0 ≤ M X i j

        MX04 — all-ones identities #

        source
        theorem BollobasNikiforov.inner_sum_right {n : Type u_1} [Fintype n] {ι : Type u_2} (B : Matrix n n ℝ) (s : Finset ι) (f : ι → Matrix n n ℝ) :
        inner B (∑ i ∈ s, f i) = ∑ i ∈ s, inner B (f i)
        source
        theorem BollobasNikiforov.isSymm_ones {n : Type u_1} :
        ones.IsSymm
        source
        theorem BollobasNikiforov.sub_single_dotProduct_one {n : Type u_1} [Fintype n] [DecidableEq n] (i j : n) :
        (e i - e j) ⬝ᵥ 1 = 0
        source
        theorem BollobasNikiforov.vecMulVec_sub_single_mulVec_one {n : Type u_1} [Fintype n] [DecidableEq n] (i j : n) :
        (Matrix.vecMulVec (e i - e j) (e i - e j)).mulVec 1 = 0
        source
        theorem BollobasNikiforov.inner_ones_vecMulVec_sub_single {n : Type u_1} [Fintype n] [DecidableEq n] (i j : n) :
        inner ones (Matrix.vecMulVec (e i - e j) (e i - e j)) = 0
        source
        theorem BollobasNikiforov.inner_ones_hadamard_self {n : Type u_1} [Fintype n] (X : Matrix n n ℝ) :
        inner ones (X.hadamard X) = inner X X
        source
        theorem BollobasNikiforov.M_mulVec_one {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) :
        (M X).mulVec 1 = (X.hadamard X).mulVec 1

        Each Laplacian annihilates the all-ones vector, so M X and X ⊙ X have the same row sums.

        source
        theorem BollobasNikiforov.inner_ones_M {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) :
        inner ones (M X) = inner X X

        MX05 — continuity and scaling #

        source
        theorem BollobasNikiforov.ite_neg_sq_eq_min_sq (x : ℝ) :
        (if x < 0 then x ^ 2 else 0) = min x 0 ^ 2
        source
        theorem BollobasNikiforov.laplacianCoeff_eq_min {n : Type u_1} [LinearOrder n] (X : Matrix n n ℝ) (i j : n) :
        laplacianCoeff X i j = if i < j then min (X i j) 0 ^ 2 else 0
        source
        theorem BollobasNikiforov.continuous_laplacianCoeff {n : Type u_1} [LinearOrder n] (i j : n) :
        Continuous fun (X : Matrix n n ℝ) => laplacianCoeff X i j
        source
        theorem BollobasNikiforov.continuous_M {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] :
        Continuous fun (X : Matrix n n ℝ) => M X
        source
        theorem BollobasNikiforov.laplacianCoeff_smul_sq {n : Type u_1} [LinearOrder n] (c : ℝ) (hc : 0 ≤ c) (X : Matrix n n ℝ) (i j : n) :
        laplacianCoeff (c ^ 2 • X) i j = c ^ 4 * laplacianCoeff X i j
        source
        theorem BollobasNikiforov.M_smul_sq {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {c : ℝ} (hc : 0 ≤ c) (X : Matrix n n ℝ) :
        M (c ^ 2 • X) = c ^ 4 • M X

        M (c² • X) = c⁴ • M X for c ≥ 0.