Whitening Equivalence for Positive Definite Symmetric Operators

Proved

FunctionalInequalities.exists_whitening_of_isSymmetric_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite-dimensional whitening existence theorem.

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

$T$ is symmetric;
$\langle Tv,v\rangle>0$ for every nonzero $v\in V$ .

Then there exists a continuous linear equivalence $W:V\simeq V$ such that $W$ is self-adjoint and

\langle T(Wu),Wv\rangle=\langle u,v\rangle\qquad\text{for all }u,v\in V.

Only existence of a self-adjoint whitening equivalence is asserted; positivity or uniqueness of $W$ is not part of the conclusion.

Original Lean declaration header

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

theorem exists_whitening_of_isSymmetric (T : V →L[ℝ] V)
    (hT : T.toLinearMap.IsSymmetric) (hpos : ∀ v, v ≠ 0 → 0 < inner ℝ (T v) v) :
    ∃ W : V ≃L[ℝ] V, (W : V →L[ℝ] V).adjoint = W ∧
      ∀ u v, inner ℝ (T (W u)) (W v) = inner ℝ u v

Module navigation

Module: Probability/Covariance/Whitening.

Source excerpt, lines 44–47 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Whitening

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

Formal statement


theorem FunctionalInequalities.exists_whitening_of_isSymmetric_readable (T : V →L[ℝ] V)
    (hT : T.toLinearMap.IsSymmetric) (hpos : ∀ v, v ≠ 0 → 0 < inner ℝ (T v) v) :
    ∃ W : V ≃L[ℝ] V, (W : V →L[ℝ] V).adjoint = W ∧
      ∀ u v, inner ℝ (T (W u)) (W v) = inner ℝ u v := by sorry

Source

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

View graph