The polar decomposition of a bounded operator

Every bounded operator T : E →L[𝕜] F between Hilbert spaces over RCLike 𝕜 factors as T = U |T|, where |T| = T.modulus is its modulus and U is a partial isometry. The canonical polar factor T.polarFactor is the continuous extension of the isometric rule |T| x ↦ T x from the range of |T| to its closure, extended by zero on the orthogonal complement. It is the canonical factor T.factorThru T.modulus of T through its modulus. No finite dimension is assumed; for linear maps between finite-dimensional spaces the corresponding factor is LinearMap.polarFactor.

The initial space of U is the closure of the range of |T|, which is (ker T)ᗮ, and its final space is the closure of the range of T; its initial and final projections U† U and U U† are the orthogonal projections onto these spaces. The polar factor is the unique bounded operator V with V |T| = T that vanishes on ker T.

The adjoint of the polar factor inverts it on the modulus, U† T = |T|, and conjugates the two moduli into each other, |T†| = T U† = U |T| U†. Consequently the polar factor of T† is U†, and T = |T†| U is the left polar decomposition. When T is injective the polar factor is an isometry, and when |T| is invertible it is T |T|⁻¹, so that it then depends continuously on T.

Main declarations

• ContinuousLinearMap.polarFactor: the canonical polar partial isometry of a bounded operator.
• ContinuousLinearMap.polarFactor_comp_modulus: the polar decomposition U |T| = T.
• ContinuousLinearMap.isPartialIsometry_polarFactor: U is a partial isometry.
• ContinuousLinearMap.ker_polarFactor, ContinuousLinearMap.range_polarFactor: ker U = ker T and the range of U is the closure of the range of T.
• ContinuousLinearMap.adjoint_polarFactor_comp_polarFactor, ContinuousLinearMap.polarFactor_comp_adjoint_polarFactor: the initial and final projections.
• ContinuousLinearMap.eq_polarFactor_iff: uniqueness of the polar factor.
• ContinuousLinearMap.modulus_adjoint: |T†| = T U†.
• ContinuousLinearMap.polarFactor_adjoint: the polar factor of T† is U†.
• ContinuousLinearMap.modulus_adjoint_comp_polarFactor: the left polar decomposition |T†| U = T.
• ContinuousLinearMap.polarFactor_eq_comp_inverse: U = T |T|⁻¹ when |T| is invertible.
• ContinuousLinearMap.norm_sub_polarFactor_le: ‖T - U‖ ≤ ‖|T| - 1‖ for an endomorphism T.
• ContinuousLinearMap.continuousOn_polarFactor: on real Hilbert spaces, U depends continuously on T where |T| is invertible.

References

• J. B. Conway, A Course in Functional Analysis, 2nd ed., Springer (1990), §VIII.3.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press (1980), Theorem VI.10.

noncomputable def ContinuousLinearMap.polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : E →L[𝕜] F

The polar factor of a bounded operator T: the canonical polar partial isometry, which sends |T| x to T x and vanishes on ker T. It is the canonical factor of T through its modulus.

theorem ContinuousLinearMap.polarFactor_eq_factorThru {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.polarFactor = T.factorThru T.modulus

The polar factor is the canonical factor of T through its modulus.

@[simp]

theorem ContinuousLinearMap.polarFactor_modulus_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (x : E) : T.polarFactor (T.modulus x) = T x

The polar factor carries the modulus of a vector to its image under T: U (|T| x) = T x.

@[simp]

theorem ContinuousLinearMap.polarFactor_comp_modulus {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.polarFactor ∘SL T.modulus = T

Polar decomposition of a bounded operator: U |T| = T.

@[simp]

theorem ContinuousLinearMap.polarFactor_apply_of_mem_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) {x : E} (hx : x ∈ (↑T).ker) : T.polarFactor x = 0

The polar factor vanishes on the kernel of T.

@[simp]

theorem ContinuousLinearMap.ker_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (↑T.polarFactor).ker = (↑T).ker

The polar factor has the same kernel as T.

theorem ContinuousLinearMap.norm_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) {x : E} (hx : x ∈ (↑T).kerᗮ) : ‖T.polarFactor x‖ = ‖x‖

The polar factor preserves norms on its initial space (ker T)ᗮ.

theorem ContinuousLinearMap.norm_polarFactor_apply_of_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : Function.Injective ⇑T) (x : E) : ‖T.polarFactor x‖ = ‖x‖

The polar factor of an injective operator is an isometry.

@[simp]

theorem ContinuousLinearMap.isPartialIsometry_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.polarFactor.IsPartialIsometry

The polar factor is a partial isometry.

theorem ContinuousLinearMap.adjoint_polarFactor_comp_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : adjoint T.polarFactor ∘SL T.polarFactor = (↑T).kerᗮ.starProjection

The initial projection U† U of the polar factor is the orthogonal projection onto (ker T)ᗮ.

@[simp]

theorem ContinuousLinearMap.range_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (↑T.polarFactor).range = (↑T).range.topologicalClosure

The range of the polar factor is the closure of the range of T.

theorem ContinuousLinearMap.polarFactor_comp_adjoint_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.polarFactor ∘SL adjoint T.polarFactor = (↑T).range.topologicalClosure.starProjection

The final projection U U† of the polar factor is the orthogonal projection onto the closure of the range of T.

theorem ContinuousLinearMap.eq_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T V : E →L[𝕜] F} (hV : V ∘SL T.modulus = T) (hV₀ : ∀ x ∈ (↑T).ker, V x = 0) : V = T.polarFactor

Uniqueness of the polar factor. A bounded operator V with V |T| = T that vanishes on ker T is the polar factor of T. It is not assumed to be a partial isometry.

theorem ContinuousLinearMap.eq_polarFactor_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) {V : E →L[𝕜] F} : V = T.polarFactor ↔ V ∘SL T.modulus = T ∧ ∀ x ∈ (↑T).ker, V x = 0

A bounded operator is the polar factor of T exactly when it factors T through its modulus and vanishes on ker T.

theorem ContinuousLinearMap.polarFactor_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {E' : Type u_4} {F' : Type u_5} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedAddCommGroup F'] [InnerProductSpace 𝕜 F'] [CompleteSpace F'] (e₁ : F ≃ₗᵢ[𝕜] F') (e₂ : E ≃ₗᵢ[𝕜] E') (T : E →L[𝕜] F) : (↑↑e₁ ∘SL T ∘SL ↑↑e₂.symm).polarFactor = ↑↑e₁ ∘SL T.polarFactor ∘SL ↑↑e₂.symm

The polar factor is natural under linear isometric equivalences of the source and target: the polar factor of e₁ T e₂⁻¹ is e₁ U e₂⁻¹. In particular the polar factor commutes with conjugation by a linear isometric equivalence.

@[simp]

theorem ContinuousLinearMap.polarFactor_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : polarFactor 0 = 0

The polar factor of the zero operator is zero.

The adjoint of the polar factor

@[simp]

theorem ContinuousLinearMap.adjoint_polarFactor_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (x : E) : (adjoint T.polarFactor) (T x) = T.modulus x

The adjoint of the polar factor carries the image of a vector back to its modulus: U† (T x) = |T| x.

@[simp]

theorem ContinuousLinearMap.adjoint_polarFactor_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : adjoint T.polarFactor ∘SL T = T.modulus

The adjoint of the polar factor carries T back to its modulus: U† T = |T|.

@[simp]

theorem ContinuousLinearMap.modulus_comp_adjoint_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.modulus ∘SL adjoint T.polarFactor = adjoint T

The adjoint of the polar decomposition: |T| U† = T†.

@[simp]

theorem ContinuousLinearMap.modulus_apply_adjoint_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (y : F) : T.modulus ((adjoint T.polarFactor) y) = (adjoint T) y

The adjoint of the polar decomposition, applied to a vector: |T| (U† y) = T† y.

theorem ContinuousLinearMap.modulus_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (adjoint T).modulus = T ∘SL adjoint T.polarFactor

The modulus of the adjoint is T composed with the adjoint of its polar factor: |T†| = T U†, equivalently |T†| = U |T| U†.

@[simp]

theorem ContinuousLinearMap.polarFactor_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (adjoint T).polarFactor = adjoint T.polarFactor

The polar factor of the adjoint is the adjoint of the polar factor.

@[simp]

theorem ContinuousLinearMap.modulus_adjoint_comp_polarFactor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (adjoint T).modulus ∘SL T.polarFactor = T

Left polar decomposition: |T†| U = T.

@[simp]

theorem ContinuousLinearMap.modulus_adjoint_apply_polarFactor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (x : E) : (adjoint T).modulus (T.polarFactor x) = T x

The left polar decomposition, applied to a vector: |T†| (U x) = T x.

Comparison with the modulus

theorem ContinuousLinearMap.polarFactor_eq_comp_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : IsUnit T.modulus) : T.polarFactor = T ∘SL Ring.inverse T.modulus

If the modulus of T is invertible, the polar factor is T |T|⁻¹.

@[simp]

theorem ContinuousLinearMap.isUnit_polarFactor {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) (hT : IsUnit T) : IsUnit T.polarFactor

The polar factor of an invertible operator is invertible.

theorem ContinuousLinearMap.norm_sub_polarFactor_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : ‖T - T.polarFactor‖ ≤ ‖T.modulus - 1‖

The polar factor U of an endomorphism T satisfies ‖T - U‖ ≤ ‖|T| - 1‖.

theorem ContinuousLinearMap.continuousOn_polarFactor {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : ContinuousOn polarFactor {T : E →L[ℝ] F | IsUnit T.modulus}

The polar factor of an operator between real Hilbert spaces depends continuously on the operator, in operator norm, wherever the modulus is invertible: there it is T |T|⁻¹.