Local Lipschitz Continuity Of Operator Inverse Square Roots

This statement establishes local Lipschitz continuity of a principal inverse-square-root operator profile.

Let E be a finite-dimensional real inner-product space and P a real normed space. Let A:P→(E→L[ℝ]E). Assume

1. $(A(p))^{-1}$ is positive for every p;
2. A(p) is a unit for every p; and
3. the map $p\mapsto(A(p))^{-1}$ is C¹.

Then

is locally Lipschitz in the operator norm, where the inverse square root is the Lean definition inverseSqrt.

This is a reusable regularity statement for parameter-dependent positive invertible operators, including localization covariance profiles.

Formalization Note The parameter space has a normed additive-group and real normed-space structure; no finite-dimensional assumption on P is present.

Original Lean declaration header

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

theorem locallyLipschitz_inverseSqrt_of_contDiff_ringInverse {P : Type*} [NormedAddCommGroup P]
    [NormedSpace ℝ P] (A : P → (E →L[ℝ] E))
    (hpos : ∀ p, (Ring.inverse (A p)).IsPositive)
    (hunit : ∀ p, IsUnit (A p))
    (hInverse : ContDiff ℝ 1 (fun p => Ring.inverse (A p))) :
    LocallyLipschitz (fun p => inverseSqrt (A p))

Module navigation

Module: Analysis/Operator/InverseSqrt.

Supporting theorems: locallyLipschitz_matrixEntries_sqrt.

Previous: locallyLipschitz_matrixEntries_sqrt.

Source excerpt, lines 223–228 · Frozen source 408915f.