The Frobenius seminorm

For a linear map A : E →ₗ[𝕜] F out of a finite-dimensional inner product space, the sum ∑ᵢ ‖A bᵢ‖² over an orthonormal basis (bᵢ) of E does not depend on the basis; when F is finite-dimensional it is the trace of A† A. Its square root is the Frobenius seminorm (the Hilbert–Schmidt norm) ‖A‖_F = √(∑ᵢ ‖A bᵢ‖²), the Euclidean norm of the tuple (A bᵢ)ᵢ. It is a unitarily invariant seminorm, and only the source needs to be finite-dimensional. When F is finite-dimensional as well, ‖A‖_F = √(∑ᵢ σᵢ(A)²) in terms of the singular values, and the Frobenius seminorm controls the nuclear seminorm with the rank-sharp constant: ‖A‖₁ ≤ √(rank A) ‖A‖_F.

In finite orthonormal source and target bases, the Frobenius seminorm equals the Frobenius norm of the rectangular coordinate matrix, and its square is the sum of the squared moduli of the matrix coefficients. This connects basis-independent operator estimates to entrywise calculations: in orthonormal eigenbases, for instance, it turns the coordinate form (αᵢ - βⱼ)Xᵢⱼ = Cᵢⱼ of a Sylvester equation AX - XB = C into the bound δ ‖X‖_F ≤ ‖C‖_F under a spectral gap δ ≤ |αᵢ - βⱼ|.

Main declarations

• LinearMap.trace_adjoint_comp_self_eq_sum_norm_apply_sq: tr (A† A) = ∑ᵢ ‖A bᵢ‖² for every orthonormal basis (bᵢ).
• LinearMap.trace_adjoint_comp_self_eq_sum_sq_singularValues: tr (A† A) = ∑ᵢ σᵢ(A)².
• LinearMap.frobenius_norm_toMatrix: the Frobenius norm of the matrix in orthonormal bases equals the operator Frobenius seminorm.
• LinearMap.sum_norm_apply_sq_eq_sum_norm_apply_sq: ∑ᵢ ‖A bᵢ‖² is independent of the orthonormal basis.
• LinearMap.sum_sq_norm_apply_orthonormal_le: compression to an orthonormal family cannot increase the squared Frobenius sum.
• TauCeti.UnitarilyInvariantSeminorm.frobenius: the Frobenius seminorm.
• TauCeti.UnitarilyInvariantSeminorm.frobenius_apply: ‖A‖_F = √(∑ᵢ ‖A bᵢ‖²) for every orthonormal basis (bᵢ).
• TauCeti.UnitarilyInvariantSeminorm.sq_frobenius_apply_eq_sum_norm_inner_sq: ‖A‖_F² = ∑ᵢ ∑ⱼ ‖⟪cⱼ, A bᵢ⟫‖² in orthonormal bases (bᵢ) of the source and (cⱼ) of the target.
• TauCeti.UnitarilyInvariantSeminorm.frobenius_apply_eq_sqrt_sum_sq_singularValues: ‖A‖_F = √(∑ᵢ σᵢ(A)²).
• TauCeti.UnitarilyInvariantSeminorm.nuclear_apply_le_sqrt_finrank_range_mul_frobenius_apply: ‖A‖₁ ≤ √(rank A) ‖A‖_F.

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section IV.2.
• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Section 5.6.

theorem LinearMap.trace_adjoint_comp_self_eq_sum_norm_apply_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (b : OrthonormalBasis ι 𝕜 E) : (trace 𝕜 E) (adjoint A ∘ₗ A) = ↑(∑ i : ι, ‖A (b i)‖ ^ 2)

The trace of A† A is ∑ᵢ ‖A bᵢ‖² for every orthonormal basis (bᵢ) of the source.

theorem LinearMap.sum_norm_apply_sq_eq_sum_norm_apply_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} {ι' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] [Fintype ι'] (A : E →ₗ[𝕜] F) (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E) : ∑ i : ι, ‖A (b i)‖ ^ 2 = ∑ i : ι', ‖A (b' i)‖ ^ 2

Basis independence of the Frobenius sum: ∑ᵢ ‖A bᵢ‖² takes the same value on any two orthonormal bases (bᵢ) and (b'ⱼ) of the source.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.frobenius (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : UnitarilyInvariantSeminorm 𝕜 E F

The Frobenius seminorm (Hilbert–Schmidt norm) ‖A‖_F = √(∑ᵢ ‖A bᵢ‖²), for any orthonormal basis (bᵢ) of the source, as a unitarily invariant seminorm.

theorem TauCeti.UnitarilyInvariantSeminorm.frobenius_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (A : E →ₗ[𝕜] F) : (frobenius 𝕜 E F) A = √(∑ i : ι, ‖A (b i)‖ ^ 2)

The Frobenius seminorm in an orthonormal basis: ‖A‖_F = √(∑ᵢ ‖A bᵢ‖²) for every orthonormal basis (bᵢ) of the source.

theorem TauCeti.UnitarilyInvariantSeminorm.sq_frobenius_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (A : E →ₗ[𝕜] F) : (frobenius 𝕜 E F) A ^ 2 = ∑ i : ι, ‖A (b i)‖ ^ 2

The square of the Frobenius seminorm is ∑ᵢ ‖A bᵢ‖² for every orthonormal basis (bᵢ) of the source.

theorem TauCeti.UnitarilyInvariantSeminorm.sq_frobenius_apply_eq_sum_norm_inner_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} {ι' : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (c : OrthonormalBasis ι' 𝕜 F) (A : E →ₗ[𝕜] F) : (frobenius 𝕜 E F) A ^ 2 = ∑ i : ι, ∑ j : ι', ‖inner 𝕜 (c j) (A (b i))‖ ^ 2

The square of the Frobenius seminorm is the sum of the squared moduli of the matrix coefficients ⟪cⱼ, A bᵢ⟫ in any orthonormal bases (bᵢ) of the source and (cⱼ) of the target.

@[simp]

theorem LinearMap.frobenius_norm_toMatrix {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {m : Type u_6} {n : Type u_7} [Fintype m] [Fintype n] [DecidableEq n] (A : E →ₗ[𝕜] F) (b : OrthonormalBasis n 𝕜 E) (c : OrthonormalBasis m 𝕜 F) : ‖(toMatrix b.toBasis c.toBasis) A‖ = (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) A

The Frobenius norm of the matrix of a rectangular operator in any orthonormal domain and codomain bases equals its unitarily invariant Frobenius seminorm.

theorem LinearMap.trace_adjoint_comp_self_eq_sum_sq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (trace 𝕜 E) (adjoint A ∘ₗ A) = ↑(A.singularValues.sum fun (x : ℕ) (s : ℝ) => s ^ 2)

The trace of A† A is the sum ∑ᵢ σᵢ(A)² of the squared singular values of A.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.frobenius_apply_eq_sqrt_sum_sq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (frobenius 𝕜 E F) A = √(A.singularValues.sum fun (x : ℕ) (s : ℝ) => s ^ 2)

The Frobenius seminorm in terms of singular values: ‖A‖_F = √(∑ᵢ σᵢ(A)²).

theorem LinearMap.sq_frobenius_apply_eq_sum_sq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) A ^ 2 = ∑ i : Fin (Module.finrank 𝕜 E), A.singularValues ↑i ^ 2

The squared Frobenius seminorm is the sum of the squared singular values.

theorem TauCeti.UnitarilyInvariantSeminorm.nuclear_apply_le_sqrt_finrank_range_mul_frobenius_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (nuclear 𝕜 E F) A ≤ √↑(Module.finrank 𝕜 ↥A.range) * (frobenius 𝕜 E F) A

Rank-sharp comparison of the nuclear and Frobenius seminorms: ‖A‖₁ ≤ √(rank A) ‖A‖_F.

theorem LinearMap.sum_sq_norm_apply_orthonormal_le {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {ι : Type u_9} {κ : Type u_10} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype ι] [Fintype κ] (M : E →ₗ[𝕜] F) (b : OrthonormalBasis ι 𝕜 E) {w : κ → E} (hw : Orthonormal 𝕜 w) : ∑ i : κ, ‖M (w i)‖ ^ 2 ≤ ∑ k : ι, ‖M (b k)‖ ^ 2

A linear map's total squared norm on an orthonormal family is bounded by its total squared norm on an orthonormal basis of the source. The target need not be finite-dimensional.

Generalized from YuWangSamworth2015/Core/Residual.lean in the Kitware DKPS formalization (Jon Crall and GPT 5.6 High; Apache-2.0), using orthonormal basis extension in place of symmetry.