Basis-defined principal inverse square roots

Definition

KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

inverseSqrtIn b A pulls back the canonical continuous-functional-calculus square root of the inverse matrix of $A$ in the orthonormal basis $b$ . inverseSqrt A uses the standard orthonormal basis of the finite-dimensional real inner-product space; these declarations define the operators but do not themselves state the positivity, inverse, uniqueness, or basis-independence properties described in the module documentation.

Original module imports

import FunctionalInequalities.Analysis.Operator.Coordinates
import FunctionalInequalities.Analysis.Operator.Positive
import Mathlib.Analysis.Calculus.ContDiff.RCLike

Original declaration excerpt

Shown in the original module context.

def inverseSqrtIn (b : OrthonormalBasis ι ℝ E) (A : E →L[ℝ] E) : E →L[ℝ] E :=
  operatorOfMatrix b (CFC.sqrt ((operatorMatrix b A)⁻¹))

Module navigation

Direct project imports: Analysis/Operator/Coordinates, Analysis/Operator/Positive.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Operator.InverseSqrt · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Coordinates
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Positive
import Mathlib.Analysis.Calculus.ContDiff.RCLike

noncomputable section
open scoped MatrixOrder RealInnerProductSpace
namespace FunctionalInequalities
namespace Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
/-- The principal (positive) inverse square root of `A` computed in the orthonormal basis `b`: the canonical
matrix `CFC.sqrt` of `(operatorMatrix b A)⁻¹`, pulled back to an operator. -/
def inverseSqrtIn (b : OrthonormalBasis ι ℝ E) (A : E →L[ℝ] E) : E →L[ℝ] E :=
  operatorOfMatrix b (CFC.sqrt ((operatorMatrix b A)⁻¹))
/-- The principal inverse square root `A^{-1/2}` (in the standard orthonormal basis; basis independent for
positive units). -/
def inverseSqrt (A : E →L[ℝ] E) : E →L[ℝ] E :=
  inverseSqrtIn (stdOrthonormalBasis ℝ E) A
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Operator/InverseSqrt.lean#L30-L109 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Operator.InverseSqrt`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt`; the repository is private at upload time).

View graph