Local Lipschitz Continuity Of Matrix Square Roots

This statement establishes local Lipschitz continuity of the canonical matrix square root.

Let X be a pseudometric space, let M:X→Matrix(ι,ι,ℝ) be continuous, and assume M(x) is positive definite for every x. If the Frobenius-coordinate map

$$x\mapsto\operatorname{matrixEntries}(M(x))$$

is locally Lipschitz, then so is

$$x\mapsto\operatorname{matrixEntries}(\sqrt{M(x)}).$$

The conclusion uses the canonical functional-calculus square root and the Frobenius norm.

This result supplies a local regularity principle for positive-definite matrix profiles.

Formalization Note The theorem is stated for finite index types with decidable equality; positivity is pointwise positive definiteness, not merely semidefiniteness.

Original Lean declaration header

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

theorem locallyLipschitz_matrixEntries_sqrt {X : Type*} [PseudoMetricSpace X]
    (M : X → Matrix ι ι ℝ) (hM : Continuous M) (hPD : ∀ x, (M x).PosDef)
    (hInput : LocallyLipschitz (fun x => matrixEntries (M x))) :
    LocallyLipschitz (fun x => matrixEntries (CFC.sqrt (M x)))

Module navigation

Module: Analysis/Operator/InverseSqrt.

Definition modules: Analysis/Matrix/Positivity.

Supporting theorems: exists_quadraticFloor_of_posDef, root_difference_bound.

Previous: inverseSqrt_mul_mul_inverseSqrt · Next: locallyLipschitz_inverseSqrt_of_contDiff_ringInverse.

Source excerpt, lines 166–169 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt

open scoped MatrixOrder RealInnerProductSpace
variable {ι : Type*} [Fintype ι] [DecidableEq ι]

theorem FunctionalInequalities.Analysis.locallyLipschitz_matrixEntries_sqrt_readable {X : Type*} [PseudoMetricSpace X]
    (M : X → Matrix ι ι ℝ) (hM : Continuous M) (hPD : ∀ x, (M x).PosDef)
    (hInput : LocallyLipschitz (fun x => matrixEntries (M x))) :
    LocallyLipschitz (fun x => matrixEntries (CFC.sqrt (M x))) := by sorry