Frobenius Positivity

If G is positive semidefinite and nonzero, and B is positive definite, then the Frobenius inner product ⟪G, B⟫ = ∑ j l, G j l * B j l is strictly positive. The proof diagonalizes B = U D Uᵀ via the spectral theorem, conjugates G to H = Uᵀ G U (which remains PSD and nonzero), and reduces to ⟪G, B⟫ = tr(H D) = ∑ i, λᵢ Hᵢᵢ > 0.

theorem frobenius_eq_trace_transpose_mul {ι : Type u} [Fintype ι] (G B : Matrix ι ι ℝ) : ∑ j : ι, ∑ l : ι, G j l * B j l = (G.transpose * B).trace

Helper: Frobenius inner product equals trace (Gᵀ * B) (real case).

theorem congr_transpose_mul_mul_ne_zero {ι : Type u} [Fintype ι] [DecidableEq ι] (U G : Matrix ι ι ℝ) (hU_right : U * U.transpose = 1) (hG_ne_zero : G ≠ 0) : U.transpose * G * U ≠ 0

Congruence by an orthogonal/invertible matrix preserves nonzeroness (real case). If U * Uᵀ = 1, then Uᵀ G U ≠ 0 whenever G ≠ 0.

theorem psd_cauchy_schwarz {ι : Type u} [Fintype ι] (H : Matrix ι ι ℝ) (hH_psd : H.PosSemidef) (x y : ι → ℝ) : (x ⬝ᵥ H.mulVec y) ^ 2 ≤ x ⬝ᵥ H.mulVec x * y ⬝ᵥ H.mulVec y

Cauchy–Schwarz for the semi-inner product induced by a PSD real matrix. For all vectors x,y: (xᵀ H y)^2 ≤ (xᵀ H x) (yᵀ H y).

theorem psd_offdiag_zero_of_diag_zero {ι : Type u} [Finite ι] (H : Matrix ι ι ℝ) (hH_psd : H.PosSemidef) {i j : ι} (hii : H i i = 0) (hjj : H j j = 0) : H i j = 0

If H is PSD over ℝ and H ii = H jj = 0 then H ij = 0.

theorem posSemidef_diag_pos_exists_of_ne_zero {ι : Type u} [Finite ι] (H : Matrix ι ι ℝ) (hH_psd : H.PosSemidef) (hH_ne_zero : H ≠ 0) : ∃ (i : ι), 0 < H i i

For a real PSD matrix, if it is nonzero then some diagonal entry is strictly positive.

theorem frobenius_pos_of_psd_posdef {ι : Type u} [Fintype ι] (G B : Matrix ι ι ℝ) (hG_psd : G.PosSemidef) (hG_ne_zero : G ≠ 0) (hB : B.PosDef) : 0 < ∑ j : ι, ∑ l : ι, G j l * B j l

Frobenius positivity for a nonzero PSD matrix against a PD matrix (real case). If G is positive semidefinite and nonzero, and B is positive definite, then the Frobenius inner product ∑ j, ∑ l, G j l * B j l is strictly positive.

High-level proof sketch (to be formalized):

• Use spectral theorem for real symmetric PD matrices: B = U D Uᵀ with D diagonal, diag(λ), λ > 0.
• Let H := Uᵀ G U. Then H is PSD and H ≠ 0 (congruence by invertible U).
• Frobenius inner product equals trace: ⟪G,B⟫ = tr(G B) = tr(H D) = ∑ i λ i * H i i.
• For PSD H, diagonal entries are ≥ 0, and H ≠ 0 ⇒ ∃ i, H i i > 0.
• Since all λ i > 0, the sum is strictly positive.
• This avoids Cholesky and uses spectral decomposition/unitary congruence invariance.