Hilbert–Schmidt Bound On Operator Application

This statement bounds the norm of an operator applied to a vector.

Let n be a natural number, let M be a continuous linear endomorphism of $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$, and let x be a vector. Then

where hsNormSq M is the squared Hilbert–Schmidt norm.

This is a standard finite-dimensional estimate useful for Lyapunov and cutoff bounds.

Formalization Note The statement uses the canonical Euclidean basis and includes all natural numbers n.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/Operator/HilbertSchmidt.

Next: opNorm_sq_le_hsNormSq.

Source excerpt, lines 76–77 · Frozen source 408915f.