Prove2Me

Hilbert–Schmidt Cauchy–Schwarz Bound

Proved
FunctionalInequalities.Analysis.sum_inner_apply_le_sqrt_hsNormSq_mul_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the Cauchy–Schwarz inequality for the Hilbert–Schmidt pairing.

Let M and N be continuous linear endomorphisms of EuclideanSpace⁡ R (Fin⁡n)\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n), and let (ej)(e_j) be the canonical orthonormal basis. Then

∑j⟨Mej,Nej⟩≤∥M∥HS2 ∥N∥HS2.\sum_j\langle Me_j,Ne_j\rangle \leq\sqrt{\|M\|_{HS}^2}\,\sqrt{\|N\|_{HS}^2}.

This is the basis-coordinate form of Cauchy–Schwarz for Hilbert–Schmidt operators.

Formalization Note The square roots are real square roots of the nonnegative quantities hsNormSq M and hsNormSq N.

Original Lean declaration header

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

theorem sum_inner_apply_le_sqrt_hsNormSq_mul (M N : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    ∑ j, ⟪M (EuclideanSpace.basisFun (Fin n) ℝ j), N (EuclideanSpace.basisFun (Fin n) ℝ j)⟫ ≤
      Real.sqrt (hsNormSq M) * Real.sqrt (hsNormSq N)

Module navigation

Module: Analysis/Operator/HilbertSchmidt.

Previous: opNorm_sq_le_hsNormSq.

Source excerpt, lines 159–161 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_HilbertSchmidt

open scoped RealInnerProductSpace
variable {n : ℕ}
Formal statement

theorem FunctionalInequalities.Analysis.sum_inner_apply_le_sqrt_hsNormSq_mul_readable (M N : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    ∑ j, ⟪M (EuclideanSpace.basisFun (Fin n) ℝ j), N (EuclideanSpace.basisFun (Fin n) ℝ j)⟫ ≤
      Real.sqrt (hsNormSq M) * Real.sqrt (hsNormSq N) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Operator/HilbertSchmidt.lean#L158-L176 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Operator.HilbertSchmidt`, declaration `FunctionalInequalities.Analysis.sum_inner_apply_le_sqrt_hsNormSq_mul`; the repository is private at upload time).

View graph