The Frobenius inner product on real matrices

Mathlib's Matrix.frobeniusNormedAddCommGroup equips Matrix m n ℝ with the Frobenius norm while keeping the topology and uniformity definitionally equal to the product ones. This file adds the compatible real inner product ⟪A, B⟫_ℝ = ∑ i, ∑ j, A i j * B i j, together with its description through the trace.

Like the Frobenius norm itself, the inner product is not a global instance, because there are several natural norms on matrices. It is registered as a scoped instance in the existing Matrix.Norms.Frobenius namespace, so open scoped Matrix.Norms.Frobenius activates the norm and the inner product together.

Main declarations

• Matrix.frobeniusInnerProductSpace — the Frobenius inner product, compatible with Matrix.frobeniusNormedAddCommGroup.
• Matrix.frobenius_inner_def — the inner product is the sum of entrywise products.
• Matrix.frobenius_inner_eq_trace_transpose_mul — the inner product is (Aᵀ * B).trace.

@[instance_reducible]

noncomputable def Matrix.frobeniusInnerProductSpace {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : InnerProductSpace ℝ (Matrix m n ℝ)

The Frobenius inner product ⟪A, B⟫_ℝ = ∑ i, ∑ j, A i j * B i j on real matrices, compatible with the Frobenius norm of Matrix.frobeniusNormedAddCommGroup. Not declared as a global instance because there are several natural choices of norm on matrices; it is available through open scoped Matrix.Norms.Frobenius.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.frobenius_inner_def {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A B : Matrix m n ℝ) : inner ℝ A B = ∑ i : m, ∑ j : n, A i j * B i j

The Frobenius inner product is the sum of the entrywise products.

theorem Matrix.frobenius_inner_eq_trace_transpose_mul {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A B : Matrix m n ℝ) : inner ℝ A B = (A.transpose * B).trace

The Frobenius inner product is the trace of Aᵀ * B.