Positive square roots and the finite-dimensional operator modulus

A positive endomorphism of a finite-dimensional real or complex inner product space has a unique positive square root. It is obtained by applying the finite symmetric functional calculus to Real.sqrt. This file develops its kernel, range, norm, and uniqueness properties, then applies the construction to the source Gram operator A† A of a rectangular map.

The resulting LinearMap.operatorAbs A is the finite-dimensional operator modulus. Its square is A† A, it has the same pointwise norms and kernel as A, and its range is (ker A)ᗮ. A normal endomorphism commutes with its modulus. These facts are the spectral input to finite-dimensional polar decomposition.

Main declarations

• LinearMap.IsPositive.sqrt: the positive square root of a positive endomorphism.
• LinearMap.IsPositive.sqrt_sq: its square is the original endomorphism.
• LinearMap.IsPositive.sqrt_unique: uniqueness among positive square roots.
• LinearMap.IsPositive.sqrt_eq_iff: the positive square root is the positive endomorphism whose square is the original endomorphism.
• LinearMap.IsPositive.commute_sqrt: an endomorphism commuting with T commutes with sqrt T.
• LinearMap.operatorAbs: the modulus sqrt (A† A) of a rectangular linear map.
• LinearMap.IsPositive.eq_operatorAbs: uniqueness among positive square roots of A† A.
• LinearMap.norm_operatorAbs_apply: ‖|A|x‖ = ‖Ax‖.
• LinearMap.ker_operatorAbs, LinearMap.range_operatorAbs: the kernel and range of the modulus.
• LinearMap.operatorAbs_injective_iff: the modulus is injective exactly when the map is.
• LinearMap.commute_operatorAbs_of_commute: an endomorphism commuting with A† A commutes with |A|.
• LinearMap.commute_operatorAbs: a normal endomorphism commutes with its modulus.
• LinearMap.operatorAbs_mul_self_of_adjoint_eq_neg, LinearMap.commute_operatorAbs_of_adjoint_eq_neg: a skew-adjoint endomorphism A satisfies |A|² = -A² and commutes with |A|.
• LinearMap.operatorAbs_comp_of_commute: |A P| = |A| P for an orthogonal projection P commuting with A† A.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Theorems 7.2.6 and 7.3.1.

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

The positive square root of a positive endomorphism, defined by the finite symmetric functional calculus at Real.sqrt.

theorem LinearMap.IsPositive.sqrt_apply_of_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) {x : E} {μ : ℝ} (hx : T x = ↑μ • x) : hT.sqrt x = ↑√μ • x

The positive square root acts on an eigenvector by the square root of its eigenvalue.

@[simp]

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) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n) : hT.sqrt ((⋯.eigenvectorBasis hn) i) = ↑√(⋯.eigenvalues hn i) • (⋯.eigenvectorBasis hn) i

The positive square root acts diagonally on the ordered eigenbasis.

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 of a positive endomorphism is positive.

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 positive square root is symmetric.

@[simp]

theorem LinearMap.IsPositive.sqrt_sq {𝕜 : 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

The square of the positive square root is the original endomorphism.

theorem LinearMap.IsPositive.norm_sqrt_apply_sq {𝕜 : 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 squared norm of sqrt T x is the quadratic form of T at x.

@[simp]

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

The positive square root has the same kernel as the original endomorphism.

@[simp]

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

The positive square root has the same range as the original endomorphism.

@[simp]

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

The positive square root is a unit exactly when the original endomorphism is a unit.

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) (hST : S ∘ₗ S = T) : S = hT.sqrt

The positive square root is unique among positive endomorphisms whose square is T.

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

The positive square root is characterized as the positive endomorphism whose square is T.

@[simp]

theorem LinearMap.IsPositive.sqrt_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : ⋯.sqrt = 0

The positive square root of the zero endomorphism is zero.

@[simp]

theorem LinearMap.IsPositive.sqrt_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : ⋯.sqrt = 1

The positive square root of the identity is the identity.

@[simp]

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

The positive square root vanishes exactly when the original endomorphism does.

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

Every endomorphism commuting with T commutes with its positive square root.

noncomputable def LinearMap.operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : E →ₗ[𝕜] E

The finite-dimensional modulus of a rectangular linear map is the positive square root of its source Gram operator A† A.

theorem LinearMap.isPositive_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs.IsPositive

The finite-dimensional modulus is positive.

theorem LinearMap.isSymmetric_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs.IsSymmetric

The finite-dimensional modulus is symmetric.

@[simp]

theorem LinearMap.operatorAbs_sq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs ∘ₗ A.operatorAbs = adjoint A ∘ₗ A

The square of the finite-dimensional modulus is the source Gram operator.

theorem LinearMap.IsPositive.eq_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {S : E →ₗ[𝕜] E} (hS : S.IsPositive) (h : S ∘ₗ S = adjoint A ∘ₗ A) : S = A.operatorAbs

The modulus is the unique positive endomorphism whose square is the source Gram operator A† A.

@[simp]

theorem LinearMap.norm_operatorAbs_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : ‖A.operatorAbs x‖ = ‖A x‖

The modulus and the original map have the same pointwise norms.

@[simp]

theorem LinearMap.ker_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs.ker = A.ker

The modulus and the original map have the same kernel.

@[simp]

theorem LinearMap.operatorAbs_injective_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} : Function.Injective ⇑A.operatorAbs ↔ Function.Injective ⇑A

The modulus of a map is injective exactly when the map is.

@[simp]

theorem LinearMap.range_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs.range = A.kerᗮ

The range of the modulus is the orthogonal complement of the original map's kernel.

theorem LinearMap.commute_operatorAbs_of_commute {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {S : E →ₗ[𝕜] E} (h : Commute S (adjoint A ∘ₗ A)) : Commute S A.operatorAbs

An endomorphism commuting with the source Gram operator A† A commutes with the modulus.

theorem LinearMap.commute_operatorAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) [IsStarNormal A] : Commute A A.operatorAbs

A normal finite-dimensional endomorphism commutes with its modulus.

theorem LinearMap.operatorAbs_mul_self_of_adjoint_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (h : adjoint A = -A) : A.operatorAbs * A.operatorAbs = -(A * A)

The modulus of a skew-adjoint finite-dimensional endomorphism squares to -A².

theorem LinearMap.commute_operatorAbs_of_adjoint_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (h : adjoint A = -A) : Commute A A.operatorAbs

A skew-adjoint finite-dimensional endomorphism commutes with its modulus.

theorem LinearMap.operatorAbs_comp_of_commute {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {P : E →ₗ[𝕜] E} (hP : P.IsSymmetricProjection) (h : Commute P (adjoint A ∘ₗ A)) : (A ∘ₗ P).operatorAbs = A.operatorAbs ∘ₗ P

If an orthogonal projection P commutes with the source Gram operator A† A, then the modulus of A P is |A| P.