The modulus of a bounded operator

For a bounded operator T : E →L[𝕜] F between Hilbert spaces over RCLike 𝕜, the source Gram operator T† T is positive, and its positive square root is the modulus |T| = √(T† T) : E →L[𝕜] E of T. The modulus measures the size of T on the source space: ‖|T| x‖ = ‖T x‖ for every x, so |T| and T have the same kernel and the same operator norm. It is the input to the polar decomposition T = U |T| of a bounded operator, whose factor U is the canonical factor T.factorThru |T| of T through its modulus.

The square root is the one of the continuous functional calculus, ContinuousLinearMap.instContinuousFunctionalCalculusRCLikeIsSelfAdjoint. That calculus is stated for a real algebra structure on E →L[𝕜] E compatible with the 𝕜-action; the definition uses ContinuousLinearMap.realAlgebra, obtained by restricting scalars along ℝ → 𝕜, so that T.modulus makes sense over every RCLike field and its API needs no structure beyond the Hilbert spaces. Any other compatible real algebra structure, such as Mathlib's own at 𝕜 = ℝ and 𝕜 = ℂ, gives the same square root (ContinuousLinearMap.modulus_eq_sqrt).

No finite dimension is assumed. For linear maps between finite-dimensional spaces the modulus LinearMap.operatorAbs is built from an eigenbasis instead.

Main declarations

• ContinuousLinearMap.modulus: the modulus |T| = √(T† T) of a bounded operator.
• ContinuousLinearMap.modulus_eq_sqrt: |T| = CFC.sqrt (T† T) for every real algebra structure compatible with the 𝕜-action; ContinuousLinearMap.modulus_eq_abs: for an endomorphism, |T| is the absolute value CFC.abs T.
• ContinuousLinearMap.isPositive_modulus, ContinuousLinearMap.isSelfAdjoint_modulus: the modulus is positive and self-adjoint.
• ContinuousLinearMap.modulus_comp_modulus: |T| |T| = T† T.
• ContinuousLinearMap.eq_modulus_iff: the modulus is the unique positive square root of T† T; in particular ContinuousLinearMap.IsPositive.modulus_eq: a positive operator is its own modulus.
• ContinuousLinearMap.norm_modulus_apply: ‖|T| x‖ = ‖T x‖; consequently ContinuousLinearMap.ker_modulus: ker |T| = ker T, ContinuousLinearMap.topologicalClosure_range_modulus: the closure of the range of |T| is (ker T)ᗮ, and ContinuousLinearMap.norm_modulus: ‖|T|‖ = ‖T‖.
• ContinuousLinearMap.commute_modulus_of_commute: an endomorphism commuting with T† T commutes with |T|.
• ContinuousLinearMap.norm_modulus_comp, ContinuousLinearMap.norm_comp_modulus: the composition laws ‖|T| D‖ = ‖T D‖ and ‖D |T|‖ = ‖D T†‖.
• ContinuousLinearMap.continuous_modulus: on real Hilbert spaces, |T| depends continuously on T.

References

• M. Reed, B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press (1980), §VI.4.

noncomputable def ContinuousLinearMap.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) : E →L[𝕜] E

The modulus |T| = √(T† T) of a bounded operator T between Hilbert spaces: the positive square root of the source Gram operator T† T.

The square root is taken in the continuous functional calculus for the real algebra structure ContinuousLinearMap.realAlgebra; ContinuousLinearMap.modulus_eq_sqrt identifies it with the square root for any other compatible real algebra structure.

theorem ContinuousLinearMap.modulus_nonneg {𝕜 : 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) : 0 ≤ T.modulus

The modulus is nonnegative in the Loewner order.

@[simp]

theorem ContinuousLinearMap.modulus_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.modulus ∘SL T.modulus = adjoint T ∘SL T

The square of the modulus is the source Gram operator: |T| |T| = T† T.

@[simp]

theorem ContinuousLinearMap.modulus_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.modulus (T.modulus x) = (adjoint T) (T x)

Applying the modulus twice is applying the source Gram operator: |T| (|T| x) = T† (T x).

theorem ContinuousLinearMap.eq_modulus_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} {S : E →L[𝕜] E} : S = T.modulus ↔ S.IsPositive ∧ S ∘SL S = adjoint T ∘SL T

Uniqueness of the modulus. The modulus is the unique positive operator whose square is the source Gram operator T† T.

theorem ContinuousLinearMap.commute_modulus_of_commute {𝕜 : 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} {S : E →L[𝕜] E} (h : Commute S (adjoint T ∘SL T)) : Commute S T.modulus

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

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

The modulus of an invertible operator is strictly positive.

theorem ContinuousLinearMap.isPositive_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.modulus.IsPositive

The modulus is positive.

theorem ContinuousLinearMap.isSelfAdjoint_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) : IsSelfAdjoint T.modulus

The modulus is self-adjoint.

@[simp]

theorem ContinuousLinearMap.adjoint_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) : adjoint T.modulus = T.modulus

The modulus is its own adjoint.

theorem ContinuousLinearMap.IsPositive.modulus_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) : T.modulus = T

A positive operator is its own modulus.

@[simp]

theorem ContinuousLinearMap.modulus_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.modulus.modulus = T.modulus

The modulus of the modulus is the modulus.

@[simp]

theorem ContinuousLinearMap.modulus_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] : modulus 0 = 0

The modulus of the zero operator is zero.

@[simp]

theorem ContinuousLinearMap.modulus_neg {𝕜 : 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 = T.modulus

An operator and its negative have the same modulus.

theorem ContinuousLinearMap.modulus_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).modulus = ↑↑e₂ ∘SL T.modulus ∘SL ↑↑e₂.symm

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

theorem ContinuousLinearMap.modulus_eq_sqrt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] (T : E →L[𝕜] F) : T.modulus = CFC.sqrt (adjoint T ∘SL T)

The modulus is the square root CFC.sqrt (T† T) of the continuous functional calculus, for every real algebra structure on E →L[𝕜] E compatible with the 𝕜-action.

theorem ContinuousLinearMap.modulus_eq_abs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] (T : E →L[𝕜] E) : T.modulus = CFC.abs T

The modulus of an endomorphism T is its absolute value CFC.abs T = √(star T * T), for every real algebra structure on E →L[𝕜] E compatible with the 𝕜-action.

@[simp]

theorem ContinuousLinearMap.norm_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.modulus x‖ = ‖T x‖

The modulus has the same pointwise norms as the operator: ‖|T| x‖ = ‖T x‖.

@[simp]

theorem ContinuousLinearMap.ker_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.modulus).ker = (↑T).ker

The modulus and the operator have the same kernel.

@[simp]

theorem ContinuousLinearMap.orthogonal_range_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.modulus).rangeᗮ = (↑T).ker

The orthogonal complement of the range of the modulus is the kernel of the operator.

@[simp]

theorem ContinuousLinearMap.topologicalClosure_range_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.modulus).range.topologicalClosure = (↑T).kerᗮ

The closure of the range of the modulus is the orthogonal complement of the kernel of the operator. This is the initial space of the polar factor of T.

@[simp]

theorem ContinuousLinearMap.norm_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.modulus‖ = ‖T‖

The modulus and the operator have the same operator norm.

@[simp]

theorem ContinuousLinearMap.norm_modulus_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] {G : Type u_4} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (T : E →L[𝕜] F) (D : G →L[𝕜] E) : ‖T.modulus ∘SL D‖ = ‖T ∘SL D‖

Precomposition law for the modulus: ‖|T| D‖ = ‖T D‖ for every bounded operator D into the source of T.

theorem ContinuousLinearMap.norm_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] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (T : E →L[𝕜] F) (D : E →L[𝕜] G) : ‖D ∘SL T.modulus‖ = ‖D ∘SL adjoint T‖

Postcomposition law for the modulus: ‖D |T|‖ = ‖D T†‖ for every bounded operator D out of the source of T into an inner product space, which need not be complete.

theorem ContinuousLinearMap.one_le_modulus_of_forall_norm_le {𝕜 : 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 : ∀ (x : E), ‖x‖ ≤ ‖T x‖) : 1 ≤ T.modulus

The modulus of a pointwise expanding Hilbert space operator is at least the identity in Loewner order.

theorem ContinuousLinearMap.isStrictlyPositive_modulus_of_forall_norm_le {𝕜 : 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 : ∀ (x : E), ‖x‖ ≤ ‖T x‖) : IsStrictlyPositive T.modulus

The modulus of a pointwise expanding Hilbert space operator is strictly positive.

theorem ContinuousLinearMap.continuous_modulus {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : Continuous modulus

The modulus of an operator between real Hilbert spaces depends continuously on the operator, in operator norm.