Asymptotically Whitening Positive Operators

Proved

FunctionalInequalities.KLS.whitening_sequence_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary lemma constructs an asymptotically identity whitening sequence.

Let $E$ be a finite-dimensional real inner-product space, and let $C_k:E\to E$ be continuous linear maps. Assume each $C_k$ is positive and that $C_k\to I$ in the operator topology. Then there exists a sequence of continuous linear equivalences $L_k:E\simeq_L E$ such that:

$L_k\to I$ in the operator topology;
for all sufficiently large $k$ , $L_k$ is self-adjoint and satisfies

L_k\,C_k\,L_k=I.

The statement provides the whitening operators used in the approximation construction.

Original Lean declaration header

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

private lemma whitening_sequence (C : ℕ → E →L[ℝ] E)
    (hpos : ∀ k, (C k).IsPositive) (hC : Tendsto C atTop (𝓝 1)) :
    ∃ L : ℕ → E ≃L[ℝ] E,
      Tendsto (fun k => (L k).toContinuousLinearMap) atTop (𝓝 1) ∧
      ∀ᶠ k in atTop,
        IsSelfAdjoint (L k).toContinuousLinearMap ∧
        (L k).toContinuousLinearMap * C k * (L k).toContinuousLinearMap = 1

Module navigation

Module: KLS/LogConcave/BallConditioning.

Supporting theorems: inverseSqrt_mul_mul_inverseSqrt.

Previous: covariance_tendsto_one · Next: exists_whitening_tendsto_moments.

Source excerpt, lines 373–379 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BallConditioning

open MeasureTheory Set Metric Filter
open scoped Topology RealInnerProductSpace MatrixOrder Matrix.Norms.L2Operator
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

Formal statement

 lemma FunctionalInequalities.KLS.whitening_sequence_readable (C : ℕ → E →L[ℝ] E)
    (hpos : ∀ k, (C k).IsPositive) (hC : Tendsto C atTop (𝓝 1)) :
    ∃ L : ℕ → E ≃L[ℝ] E,
      Tendsto (fun k => (L k).toContinuousLinearMap) atTop (𝓝 1) ∧
      ∀ᶠ k in atTop,
        IsSelfAdjoint (L k).toContinuousLinearMap ∧
        (L k).toContinuousLinearMap * C k * (L k).toContinuousLinearMap = 1 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/BallConditioning.lean#L373-L455 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.BallConditioning`, declaration `_private.FunctionalInequalities.KLS.LogConcave.BallConditioning.0.FunctionalInequalities.KLS.whitening_sequence`; the repository is private at upload time).

View graph