The ℓ² operator norm as a normed real algebra

Mathlib's scoped ℓ² operator norm (Matrix.Norms.L2Operator) makes Matrix n n 𝕜 a normed 𝕜-algebra, for 𝕜 = ℝ or ℂ (any RCLike field). Results about continuous functional calculi and the exponential stated over ℝ additionally need a normed ℝ-algebra structure on Matrix n n 𝕜. This file provides it, extending the existing ℝ-algebra structure on matrices rather than restricting scalars, so that no algebra diamond arises.

Main definitions

• Matrix.l2OpNormedAlgebraReal: Matrix n n 𝕜 with the ℓ² operator norm, as a normed ℝ-algebra.

Main results

• Matrix.norm_apply_le_l2_opNorm: an entrywise bound, including rectangular matrices.
• Matrix.l2_opNorm_one_le: an identity bound that also applies to empty matrices.
• Matrix.norm_trace_le_card_mul_l2_opNorm and Matrix.norm_normalized_trace_le_l2_opNorm: trace and normalized trace bounds.

theorem Matrix.norm_apply_le_l2_opNorm {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {m : Type u_3} [Fintype m] (A : Matrix m n 𝕜) (i : m) (j : n) : ‖A i j‖ ≤ ‖A‖

Every entry is bounded by the Euclidean operator norm.

theorem Matrix.l2_opNorm_one_le {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] : ‖1‖ ≤ 1

The norm of the identity is at most one, also when the index type is empty.

theorem Matrix.norm_trace_le_card_mul_l2_opNorm {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) : ‖M.trace‖ ≤ ↑(Fintype.card n) * ‖M‖

The trace is bounded by the dimension times the Euclidean operator norm.

theorem Matrix.norm_normalized_trace_le_l2_opNorm {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) : ‖(↑(Fintype.card n))⁻¹ * M.trace‖ ≤ ‖M‖

The absolute normalized trace is at most the Euclidean operator norm, including in dimension zero.

@[reducible, inline]

noncomputable abbrev Matrix.l2OpNormedAlgebraReal {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] : NormedAlgebra ℝ (Matrix n n 𝕜)

Matrix n n 𝕜 with the ℓ² operator norm, as a normed ℝ-algebra. It extends the existing ℝ-algebra structure rather than restricting scalars, so that no algebra diamond arises.