The Hilbert–Schmidt inner product on matrices

The Hilbert–Schmidt (Frobenius) inner product of two complex matrices is ⟪A, B⟫ = Tr[Aᴴ B]. Mathlib equips Matrix with the Frobenius norm but not (as a global instance) with this inner product, so this quantum-free helper records the plain bilinear data needed downstream: conjugate symmetry, sesquilinearity, and — the key fact for the Lie-algebraic variance formula — multiplicativity over the Kronecker product, ⟪A ⊗ C, B ⊗ D⟫ = ⟪A, B⟫ · ⟪C, D⟫.

(The genuine InnerProductSpace structure, when needed for Gram–Schmidt / orthonormal bases, is obtained separately by transport along the linear isometry to EuclideanSpace ℂ (m × m).)

def QuantumAlg.hsInner {m : Type u_1} [Fintype m] (A B : Matrix m m ℂ) : ℂ

The Hilbert–Schmidt (Frobenius) inner product ⟪A, B⟫ = Tr[Aᴴ B]. Conjugate-linear in the first argument, linear in the second.

Equations

• QuantumAlg.hsInner A B = (A.conjTranspose * B).trace

@[simp]

theorem QuantumAlg.hsInner_def {m : Type u_1} [Fintype m] (A B : Matrix m m ℂ) : hsInner A B = (A.conjTranspose * B).trace

theorem QuantumAlg.hsInner_conj_symm {m : Type u_1} [Fintype m] (A B : Matrix m m ℂ) : hsInner A B = (starRingEnd ℂ) (hsInner B A)

Conjugate symmetry: ⟪A, B⟫ = conj ⟪B, A⟫.

theorem QuantumAlg.hsInner_add_right {m : Type u_1} [Fintype m] (A B C : Matrix m m ℂ) : hsInner A (B + C) = hsInner A B + hsInner A C

Additivity in the second argument.

theorem QuantumAlg.hsInner_add_left {m : Type u_1} [Fintype m] (A B C : Matrix m m ℂ) : hsInner (A + B) C = hsInner A C + hsInner B C

Additivity in the first argument.

theorem QuantumAlg.hsInner_sub_right {m : Type u_1} [Fintype m] (A B C : Matrix m m ℂ) : hsInner A (B - C) = hsInner A B - hsInner A C

Subtractivity in the second argument.

theorem QuantumAlg.hsInner_sub_left {m : Type u_1} [Fintype m] (A B C : Matrix m m ℂ) : hsInner (A - B) C = hsInner A C - hsInner B C

Subtractivity in the first argument.

theorem QuantumAlg.hsInner_smul_right {m : Type u_1} [Fintype m] (c : ℂ) (A B : Matrix m m ℂ) : hsInner A (c • B) = c * hsInner A B

Linearity in the second argument.

theorem QuantumAlg.hsInner_smul_left {m : Type u_1} [Fintype m] (c : ℂ) (A B : Matrix m m ℂ) : hsInner (c • A) B = (starRingEnd ℂ) c * hsInner A B

Conjugate-linearity in the first argument.

theorem QuantumAlg.hsInner_sum_right {m : Type u_1} [Fintype m] {ι : Type u_2} (A : Matrix m m ℂ) (s : Finset ι) (f : ι → Matrix m m ℂ) : hsInner A (∑ i ∈ s, f i) = ∑ i ∈ s, hsInner A (f i)

Additivity over a finite sum in the second argument.

theorem QuantumAlg.hsInner_sum_left {m : Type u_1} [Fintype m] {ι : Type u_2} (s : Finset ι) (f : ι → Matrix m m ℂ) (B : Matrix m m ℂ) : hsInner (∑ i ∈ s, f i) B = ∑ i ∈ s, hsInner (f i) B

Additivity over a finite sum in the first argument.

theorem QuantumAlg.hsInner_kronecker {m : Type u_1} [Fintype m] {n : Type u_2} [Fintype n] (A B : Matrix m m ℂ) (C D : Matrix n n ℂ) : hsInner (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A C) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B D) = hsInner A B * hsInner C D

Multiplicativity over the Kronecker product — the key identity for assembling the quadratic Casimir's inner products: ⟪A ⊗ C, B ⊗ D⟫ = ⟪A, B⟫ · ⟪C, D⟫.

theorem QuantumAlg.hsInner_comm_of_isHermitian {m : Type u_1} [Fintype m] {A B : Matrix m m ℂ} (hA : A.conjTranspose = A) (hB : B.conjTranspose = B) : hsInner A B = hsInner B A

For Hermitian arguments the Hilbert–Schmidt inner product is symmetric.

theorem QuantumAlg.hsInner_conj_of_isHermitian {m : Type u_1} [Fintype m] {A B : Matrix m m ℂ} (hA : A.conjTranspose = A) (hB : B.conjTranspose = B) : (starRingEnd ℂ) (hsInner A B) = hsInner A B

For Hermitian arguments the Hilbert–Schmidt inner product is real.

theorem QuantumAlg.hsInner_single {m : Type u_1} [Fintype m] [DecidableEq m] (i j k l : m) : hsInner (Matrix.single i j 1) (Matrix.single k l 1) = if i = k ∧ j = l then 1 else 0

The matrix units single i j 1 are Hilbert–Schmidt orthonormal.