The entrywise bound for the L2 operator norm

Category: 1-Mathlib (CSD-free, staged for upstream).

Matrix.norm_entry_le_l2_opNorm: every entry of a matrix is bounded in norm by the L2 operator norm, ‖M a b‖ ≤ ‖M‖. The entry is a coordinate of the image of a unit basis vector, M a b = (M *ᵥ e_b) a, a Euclidean coordinate is at most the Euclidean norm, and l2_opNorm_mulVec bounds the image norm.

This is the bridge from operator-norm estimates (e.g. the Duhamel bound Matrix.norm_exp_smul_neg_I_sub_le) to entrywise continuity statements, which live in the Matrix Pi topology and therefore compose with topology-agnostic downstream API without touching the scoped Matrix.Norms.L2Operator instances.

Provenance

Staged as upstream Mathlib material. Intended location: Mathlib/Analysis/CStarAlgebra/Matrix.lean (beside entry_norm_bound_of_unitary, which is the special case of a unitary matrix combined with l2_opNorm_of_unitary).

Tags

matrix, operator norm, entrywise bound

theorem EuclideanSpace.norm_coord_le_norm {m : Type u_1} [Fintype m] {𝕜 : Type u_3} [RCLike 𝕜] (v : EuclideanSpace 𝕜 m) (a : m) : ‖v.ofLp a‖ ≤ ‖v‖

A Euclidean coordinate is at most the Euclidean norm.

theorem Matrix.norm_entry_le_l2_opNorm {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] {𝕜 : Type u_3} [RCLike 𝕜] (M : Matrix m n 𝕜) (a : m) (b : n) : ‖M a b‖ ≤ ‖M‖

Every matrix entry is bounded by the L2 operator norm: ‖M a b‖ ≤ ‖M‖.