Operator Norm Bounded By Hilbert–Schmidt Norm

This statement compares two norms of a finite-dimensional operator.

Let M be a continuous linear endomorphism of $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$. Then

where hsNormSq M denotes the squared Hilbert–Schmidt norm.

This is a basic norm comparison reusable in finite-dimensional operator estimates.

Formalization Note The result is stated for every natural number n and uses the operator norm supplied by the continuous-linear-map structure.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem opNorm_sq_le_hsNormSq (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    ‖M‖ ^ 2 ≤ hsNormSq M

Module navigation

Module: Analysis/Operator/HilbertSchmidt.

Supporting theorems: norm_apply_sq_le_hsNormSq_mul.

Previous: norm_apply_sq_le_hsNormSq_mul · Next: sum_inner_apply_le_sqrt_hsNormSq_mul.

Source excerpt, lines 106–107 · Frozen source 408915f.