Frobenius pairing, entrywise positive part, and the Schur product

This file records the real Frobenius inner product ⟨B, C⟩ = tr(Bᵀ C), the entrywise positive part of a matrix, the rank-one Laplacian vecMulVec (e i - e j) (e i - e j), and the Schur product theorem for real positive semidefinite matrices.

N06 — Frobenius pairing

def BollobasNikiforov.inner {n : Type u_2} [Fintype n] (B C : Matrix n n ℝ) : ℝ

The real Frobenius pairing ⟨B, C⟩ = tr(Bᵀ C).

Equations

• BollobasNikiforov.inner B C = (B.transpose * C).trace

theorem BollobasNikiforov.inner_comm {n : Type u_2} [Fintype n] (B C : Matrix n n ℝ) : inner B C = inner C B

The Frobenius pairing is symmetric.

theorem BollobasNikiforov.inner_add_left {n : Type u_2} [Fintype n] (B₁ B₂ C : Matrix n n ℝ) : inner (B₁ + B₂) C = inner B₁ C + inner B₂ C

The Frobenius pairing is additive in the first argument.

theorem BollobasNikiforov.inner_add_right {n : Type u_2} [Fintype n] (B C₁ C₂ : Matrix n n ℝ) : inner B (C₁ + C₂) = inner B C₁ + inner B C₂

The Frobenius pairing is additive in the second argument.

theorem BollobasNikiforov.inner_smul_left {n : Type u_2} [Fintype n] (r : ℝ) (B C : Matrix n n ℝ) : inner (r • B) C = r * inner B C

The Frobenius pairing is homogeneous in the first argument.

theorem BollobasNikiforov.inner_smul_right {n : Type u_2} [Fintype n] (r : ℝ) (B C : Matrix n n ℝ) : inner B (r • C) = r * inner B C

The Frobenius pairing is homogeneous in the second argument.

theorem BollobasNikiforov.inner_eq_sum {n : Type u_2} [Fintype n] (B C : Matrix n n ℝ) : inner B C = ∑ i : n, ∑ j : n, B i j * C i j

Expanding the Frobenius pairing as an entrywise sum. This identity does not require symmetry of either argument; in particular it yields the Frobenius–Hadamard formula for a symmetric first factor.

theorem BollobasNikiforov.inner_self {n : Type u_2} [Fintype n] (B : Matrix n n ℝ) : inner B B = ∑ i : n, ∑ j : n, B i j ^ 2

The squared Frobenius norm is the sum of squares of entries.

N08 — Entrywise positive part

def BollobasNikiforov.posPart {m : Type u_1} {n : Type u_2} (X : Matrix m n ℝ) : Matrix m n ℝ

The entrywise positive part (posPart X) i j = max (X i j) 0.

Equations

• BollobasNikiforov.posPart X = Matrix.of fun (i : m) (j : n) => max (X i j) 0

@[simp]

theorem BollobasNikiforov.posPart_apply {m : Type u_1} {n : Type u_2} (X : Matrix m n ℝ) (i : m) (j : n) : posPart X i j = max (X i j) 0

theorem BollobasNikiforov.posPart_nonneg {m : Type u_1} {n : Type u_2} (X : Matrix m n ℝ) (i : m) (j : n) : 0 ≤ posPart X i j

theorem BollobasNikiforov.posPart_eq_of_nonneg {m : Type u_1} {n : Type u_2} (X : Matrix m n ℝ) {i : m} {j : n} (h : 0 ≤ X i j) : posPart X i j = X i j

N09 — Rank-one Laplacian entries

def BollobasNikiforov.e {n : Type u_2} [DecidableEq n] (k : n) : n → ℝ

The standard basis vector e k in n → ℝ.

Equations

• BollobasNikiforov.e k = Pi.single k 1

theorem BollobasNikiforov.sub_single_apply {n : Type u_2} [DecidableEq n] {i j : n} (hij : i ≠ j) (a : n) : (e i - e j) a = if a = i then 1 else if a = j then -1 else 0

The vector e i - e j in coordinates.

theorem BollobasNikiforov.vecMulVec_sub_single_apply {n : Type u_2} [DecidableEq n] {i j : n} (hij : i ≠ j) (a b : n) : Matrix.vecMulVec (e i - e j) (e i - e j) a b = if a = i ∧ b = i then 1 else if a = j ∧ b = j then 1 else if a = i ∧ b = j then -1 else if a = j ∧ b = i then -1 else 0

Entries of the rank-one Laplacian vecMulVec (e i - e j) (e i - e j).

N10 — Inner product against a rank-one Laplacian

theorem BollobasNikiforov.inner_vecMulVec_sub_single {n : Type u_2} [Fintype n] [DecidableEq n] {C : Matrix n n ℝ} (hC : C.IsSymm) {i j : n} (hij : i ≠ j) : inner C (Matrix.vecMulVec (e i - e j) (e i - e j)) = C i i + C j j - 2 * C i j

N14 — Schur product of PSD matrices

theorem BollobasNikiforov.mul_diagonal_mul_transpose_apply {n : Type u_2} [Fintype n] [DecidableEq n] (U : Matrix n n ℝ) (d : n → ℝ) (a b : n) : (U * Matrix.diagonal d * U.transpose) a b = ∑ k : n, d k * U a k * U b k

theorem BollobasNikiforov.mul_diagonal_mul_transpose_eq_sum_smul_vecMulVec {n : Type u_2} [Fintype n] [DecidableEq n] (U : Matrix n n ℝ) (d : n → ℝ) : U * Matrix.diagonal d * U.transpose = ∑ k : n, d k • Matrix.vecMulVec (U.col k) (U.col k)

theorem BollobasNikiforov.isHermitian_eq_sum_smul_vecMulVec {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) : A = ∑ k : n, hA.eigenvalues k • Matrix.vecMulVec ((↑hA.eigenvectorUnitary).col k) ((↑hA.eigenvectorUnitary).col k)

The unitary diagonalization of a real Hermitian matrix expands as a sum of real rank-one terms.

theorem BollobasNikiforov.hadamard_vecMulVec_eq_diagonal_mul {n : Type u_2} [Fintype n] [DecidableEq n] (v : n → ℝ) (Y : Matrix n n ℝ) : (Matrix.vecMulVec v v).hadamard Y = Matrix.diagonal v * Y * Matrix.diagonal v

Hadamard product against a real rank-one matrix is a diagonal congruence.

theorem BollobasNikiforov.hadamard_sum {m : Type u_1} {n : Type u_2} {ι : Type u_3} (s : Finset ι) (f : ι → Matrix m n ℝ) (Y : Matrix m n ℝ) : (∑ i ∈ s, f i).hadamard Y = ∑ i ∈ s, (f i).hadamard Y

theorem BollobasNikiforov.posSemidef_diagonal_mul_mul_diagonal {n : Type u_2} [Fintype n] [DecidableEq n] {Y : Matrix n n ℝ} (hY : Y.PosSemidef) (v : n → ℝ) : (Matrix.diagonal v * Y * Matrix.diagonal v).PosSemidef

A real diagonal congruence preserves positive semidefiniteness.

theorem BollobasNikiforov.posSemidef_hadamard {n : Type u_2} [Finite n] {X Y : Matrix n n ℝ} (hX : X.PosSemidef) (hY : Y.PosSemidef) : (X.hadamard Y).PosSemidef

Schur product theorem (real PSD version): the Hadamard product of positive semidefinite matrices is positive semidefinite.

theorem BollobasNikiforov.posSemidef_hadamard_self {n : Type u_2} [Finite n] {X : Matrix n n ℝ} (hX : X.PosSemidef) : (X.hadamard X).PosSemidef

The entrywise square of a real PSD matrix is PSD.