The positive square root of a positive symmetric operator (Sub-dev I)

For a positive symmetric operator T on a finite-dimensional inner product space over 𝕜 : RCLike, we build the unique positive symmetric operator sqrt T with sqrt T ∘ₗ sqrt T = T, via the spectral theorem (sqrt T := ∑ᵢ √λᵢ • rankOne eᵢ eᵢ).

Source: Horn & Johnson, Matrix Analysis, 2nd ed. (2013), Theorem 7.2.6 (unique positive semidefinite square root) and Theorem 7.2.7(b) (ker (A⋆A) = ker A).

This is the 𝕜-generic (ℝ and ℂ) LinearMap counterpart of mathlib's ℂ-only CFC.sqrt/CFC.abs on E →L[ℂ] E; the RCLike operator route needs it because the C⋆-algebra/CFC instances on E →L[𝕜] E are registered only for 𝕜 = ℂ.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.PositiveSqrt, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 3676b55.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Opus 4.8; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

LinearMap.IsPositive.sqrt itself is defined in ForTauCeti/Analysis/InnerProductSpace/SelfAdjointFunctionalCalculus.lean, as the functional calculus of Real.sqrt. It was once defined twice -- there and here, with the two shown equal by rfl -- and the duplicate has since been collapsed into the calculus. This module keeps what is special to the square root — that it is positive, that it squares to T, and the uniqueness theory the general calculus has no analogue for.

theorem LinearMap.IsPositive.sqrt_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : hT.sqrt.IsPositive

The square root is positive. HJ 7.2.6 (it is the PSD square root).

theorem LinearMap.IsPositive.sqrt_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : hT.sqrt.IsSymmetric

The square root is symmetric.

theorem LinearMap.IsPositive.sqrt_apply_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (k : Fin (Module.finrank 𝕜 E)) : hT.sqrt ((⋯.eigenvectorBasis ⋯) k) = ↑√(⋯.eigenvalues ⋯ k) • (⋯.eigenvectorBasis ⋯) k

sqrt T acts on the k-th eigenvector as multiplication by √λₖ (it is diagonal in the same eigenbasis as T).

theorem LinearMap.IsPositive.sqrt_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : hT.sqrt ∘ₗ hT.sqrt = T

Defining property: sqrt T squares to T. HJ 7.2.6 (B² = A).

theorem LinearMap.IsPositive.apply_eq_smul_of_apply_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsPositive) {v : E} {μ : ℝ} (hμ : 0 ≤ μ) (hv : S (S v) = (↑μ * ↑μ) • v) : S v = ↑μ • v

Pointwise root: if S ≥ 0 and S² v = μ² v with μ ≥ 0, then S v = μ v. The crux of uniqueness — v lies in the μ²-eigenspace of S², on which the positive S acts as μ.

theorem LinearMap.IsPositive.sqrt_unique {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) (h : S ∘ₗ S = T) : S = hT.sqrt

Uniqueness: any positive S with S² = T is sqrt T. HJ 7.2.6(a).

@[simp]

theorem LinearMap.IsPositive.sq_norm_sqrt_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) : ‖hT.sqrt x‖ ^ 2 = RCLike.re (inner 𝕜 (T x) x)

The isometry-defect identity ‖sqrt T x‖² = re ⟪T x, x⟫. This is the seed of the polar decomposition norm identity ‖A x‖ = ‖|A| x‖.

theorem LinearMap.IsPositive.ker_sqrt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : hT.sqrt.ker = T.ker

ker (sqrt T) = ker T. HJ 7.2.7(b) applied through sqrt T ∘ₗ sqrt T = T.

theorem LinearMap.IsPositive.range_sqrt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : hT.sqrt.range = T.range

range (sqrt T) = range T. HJ 7.2.6(c).

theorem LinearMap.IsPositive.isUnit_sqrt_of_isUnit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (hunit : IsUnit T) : IsUnit hT.sqrt

On the invertible (strictly positive) case, sqrt T is invertible; this provides the inverse square root used by the intertwining unitary.