Norm Factorization of a Positive Symmetric Quadratic Form

Proved

FunctionalInequalities.exists_norm_sq_eq_inner_of_isSymmetric_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This constructs a norm factor for a positive symmetric operator.

Let $V$ be a finite-dimensional real inner-product space and let $T:V\to V$ be a continuous linear map. Assume:

$T$ is symmetric;
its quadratic form is nonnegative:

0\le\langle Tv,v\rangle\qquad\text{for every }v\in V.

Then there exists a continuous linear map $B:V\to V$ such that

\langle Tv,v\rangle=\|Bv\|^2 \qquad\text{for every }v\in V.

Only existence of $B$ is asserted; it need not be stated symmetric, unique, or positive.

The result provides the abstract square-root-type factorization used to represent covariance energies by weighted gradients.

Original Lean declaration header

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

theorem exists_norm_sq_eq_inner_of_isSymmetric (T : V →L[ℝ] V)
    (hT : T.toLinearMap.IsSymmetric) (hpos : ∀ v, 0 ≤ inner ℝ (T v) v) :
    ∃ B : V →L[ℝ] V, ∀ v, inner ℝ (T v) v = ‖B v‖ ^ 2

Module navigation

Module: Probability/Covariance/Factorization.

Source excerpt, lines 32–34 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Factorization

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.exists_norm_sq_eq_inner_of_isSymmetric_readable (T : V →L[ℝ] V)
    (hT : T.toLinearMap.IsSymmetric) (hpos : ∀ v, 0 ≤ inner ℝ (T v) v) :
    ∃ B : V →L[ℝ] V, ∀ v, inner ℝ (T v) v = ‖B v‖ ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Covariance/Factorization.lean#L31-L65 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Covariance.Factorization`, declaration `FunctionalInequalities.exists_norm_sq_eq_inner_of_isSymmetric`; the repository is private at upload time).

View graph