Inverse Square Root Root Sandwich
ProvedFunctionalInequalities.Analysis.inverseSqrt_mul_mul_inverseSqrt_readableThis formalizes part of equation (67) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), concerning the inverse-square-root diffusion coefficient.
Let E be a finite-dimensional real inner-product space and let A:E→E be a positive continuous linear operator that is a unit. Let σ=inverseSqrt A be its principal inverse square root. Then
Thus the inverse square root whitens A in the operator product, without any commutation assumption being added to the statement.
This identity is reusable in covariance normalization and localization arguments involving positive invertible operators.
Formalization Note The identity uses composition and multiplication of continuous linear maps; IsPositive and IsUnit are the exact Lean hypotheses.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem inverseSqrt_mul_mul_inverseSqrt (A : E →L[ℝ] E) (hpos : A.IsPositive) (hunit : IsUnit A) :
inverseSqrt A * A * inverseSqrt A = 1
Module navigation
Module: Analysis/Operator/InverseSqrt.
Next: locallyLipschitz_matrixEntries_sqrt.
Source excerpt, lines 130–131 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
theorem FunctionalInequalities.Analysis.inverseSqrt_mul_mul_inverseSqrt_readable (A : E →L[ℝ] E) (hpos : A.IsPositive) (hunit : IsUnit A) :
inverseSqrt A * A * inverseSqrt A = 1 := by sorry