Real Continuous-Functional-Calculus Square-Root Bridge

This is an auxiliary bridge between the matrix square-root construction CFC.sqrt and the real continuous functional calculus.

Let $\iota$ be a finite index type with decidable equality, and let $M$ be a real symmetric matrix indexed by $\iota$. Then:

1. $M^2$ is positive semidefinite;
2. its matrix square root agrees with the real functional-calculus expression;
3. $\operatorname{CFC.sqrt}(M^2)$ is positive semidefinite;
4. the square root of this matrix again agrees with the corresponding real functional-calculus expression.

Explicitly,

and

The result supplies the square-root identities needed for the spectral sign factorization.

Formalization Note Positivity is expressed by matrix order, and no positivity assumption on $M$ itself is required.

Original Lean declaration header

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

theorem symmetric_matrix_sqrt_real_cfc_bridge
    (M : Matrix ι ι ℝ) (hM : M.IsSymm) :
    0 ≤ M * M ∧
      CFC.sqrt (M * M) = cfc (fun x : ℝ => Real.sqrt x) (M * M) ∧
      0 ≤ CFC.sqrt (M * M) ∧
      CFC.sqrt (CFC.sqrt (M * M)) =
        cfc (fun x : ℝ => Real.sqrt x) (CFC.sqrt (M * M))

Module navigation

Module: Analysis/Matrix/Sign.

Next: symmetric_matrix_sign_factorization.

Source excerpt, lines 43–49 · Frozen source 408915f.