The diagonal bound for the L2 operator norm

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

Matrix.l2_opNorm_diagonal_le: a diagonal matrix with uniformly bounded entries has L2 operator norm at most that bound, (∀ i, ‖w i‖ ≤ C) → ‖diagonal w‖ ≤ C. The action of diagonal w is coordinatewise multiplication, so the image's Euclidean norm is bounded factor-by-factor. Only the ≤ direction is staged — it is what operator-norm pricing consumes (CV/InteractionPrice.lean, the CV-9 Duhamel route); the equality (= ⨆ i, ‖w i‖) is a separate upstream item.

Provenance

Staged as upstream Mathlib material. Intended location: Mathlib/Analysis/CStarAlgebra/Matrix.lean beside l2_opNorm_mulVec.

Tags

matrix, operator norm, diagonal

theorem Matrix.l2_opNorm_diagonal_le {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [RCLike 𝕜] (w : n → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : n), ‖w i‖ ≤ C) : ‖diagonal w‖ ≤ C

A diagonal matrix with uniformly bounded entries has L2 operator norm at most that bound: (∀ i, ‖w i‖ ≤ C) → ‖diagonal w‖ ≤ C.