The modulus of a Hilbert-space operator

For a bounded operator T : E →L[𝕜] F between Hilbert spaces over 𝕜 : RCLike, its modulus |T| = (T⋆ T)^(1/2) is the positive square root, through the continuous functional calculus, of the Gram operator T⋆ T acting on the source space E.

The definition is stated for a general (rectangular) T: the source space alone determines the construction, and the endomorphism case F = E is a specialization rather than a separate definition (modulus_eq_sqrt_star_mul_self, modulus_mul_self_eq_star_mul_self).

Scalar infrastructure

CFC.sqrt is a statement about the real algebra E →L[𝕜] E. For an arbitrary RCLike 𝕜, the required real algebra, scalar tower, and real self-adjoint continuous functional calculus are canonical constructions in ForTauCeti. They are activated here as low-priority local instances. They are intentionally not global instances: making the extra real scalar action globally visible changes elaboration of scalar multiplication in unrelated operator proofs.

Consequently the public modulus API below has only the mathematical Hilbert-space and completeness assumptions. Callers do not supply Algebra ℝ (E →L[𝕜] E), IsScalarTower ℝ 𝕜 (E →L[𝕜] E), or a continuous-functional-calculus instance.

Its finite-dimensional counterpart. TauCeti.operatorAbs in ForTauCeti/Analysis/InnerProductSpace/Polar/Decomposition.lean is the finite-dimensional RCLike modulus, built from the spectral square root rather than from the continuous functional calculus. It is rectangular as well: for A : E →ₗ[𝕜] F, operatorAbs A acts on the source E. Polar/CFCBridge.lean proves that its bounded realization agrees with modulus.

Main results

• ContinuousLinearMap.modulus_mul_self: the defining identity |T| * |T| = T⋆ T;
• ContinuousLinearMap.eq_modulus_of_nonneg_of_mul_self_eq: |T| is the unique nonnegative square root of the Gram operator;
• ContinuousLinearMap.norm_modulus_apply: the pointwise isometry ‖|T| x‖ = ‖T x‖, from which ContinuousLinearMap.norm_modulus (‖|T|‖ = ‖T‖) and the one-sided composition laws ContinuousLinearMap.norm_modulus_comp (‖|T| ∘L D‖ = ‖T ∘L D‖) and ContinuousLinearMap.norm_comp_modulus (‖D ∘L |T|‖ = ‖D ∘L T⋆‖) follow;
• ContinuousLinearMap.modulus_apply_eq_zero_iff: |T| x = 0 ↔ T x = 0;
• ContinuousLinearMap.modulus_commute_modulus: moduli of operators with commuting Gram operators commute.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original modules: DavisKahan/OperatorIdeal/ApproximationNumbers/OperatorModulus.lean (rectangularOperatorModulus and its API, Jon Crall / OpenAI GPT-5.6 Thinking) and ForMathlib/Analysis/InnerProductSpace/OperatorAbsoluteValue.lean (operatorAbs and its API, Jon Crall / Claude Fable 5), both at Davis--Kahan commit fc38eb4; Apache 2.0.
• Extraction class: unified and generalized. Per the signature-polish backlog, the two parallel APIs — one rectangular, one square — are replaced by this single rectangular definition with dot notation on ContinuousLinearMap. The square-only composition laws norm_operatorAbs_mul / norm_mul_operatorAbs are generalized to rectangular operators here, and reproved from the pointwise isometry instead of the C⋆-identity; the uniqueness and commutation results are likewise generalized.
• Spectra influence: none — the construction uses Mathlib together with the reusable ForTauCeti scalar-transport functional calculus.

theorem ContinuousLinearMap.adjoint_comp_self_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : 0 ≤ adjoint T ∘SL T

The Gram operator T⋆ T is nonnegative. This is the 0 ≤ · form of ContinuousLinearMap.isPositive_adjoint_comp_self.

Local scalar and functional-calculus instances

noncomputable def ContinuousLinearMap.modulus {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : E →L[𝕜] E

The modulus |T| = (T⋆ T)^(1/2) of a bounded operator between Hilbert spaces: the positive square root, through the continuous functional calculus, of the Gram operator T⋆ T on the source space.

Equations

• T.modulus = CFC.sqrt (ContinuousLinearMap.adjoint T ∘SL T)

theorem ContinuousLinearMap.modulus_def {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.modulus = CFC.sqrt (adjoint T ∘SL T)

The modulus unfolded. The characteristic lemma: |T| is the functional calculus square root of the Gram operator. A consumer in another module that needs to rewrite through the definition should use this rather than rw [modulus], which only works while the body is exposed.

modulus_eq_sqrt_star_mul_self is the endomorphism specialization, in C⋆-algebra notation.

@[simp]

theorem ContinuousLinearMap.modulus_neg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : (-T).modulus = T.modulus

The modulus is insensitive to multiplication by -1.

theorem ContinuousLinearMap.modulus_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [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 C⋆-order.

theorem ContinuousLinearMap.modulus_isSelfAdjoint {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [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} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : adjoint T.modulus = T.modulus

The modulus is self-adjoint, being a positive square root.

theorem ContinuousLinearMap.modulus_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.modulus * T.modulus = adjoint T ∘SL T

The defining identity |T| * |T| = T⋆ T.

theorem ContinuousLinearMap.eq_modulus_of_nonneg_of_mul_self_eq {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {b : E →L[𝕜] E} (hb : 0 ≤ b) (h : b * b = adjoint T ∘SL T) : b = T.modulus

The modulus is the unique nonnegative square root of the Gram operator.

@[simp]

theorem ContinuousLinearMap.norm_modulus_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [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 is a pointwise isometry onto the values of T: ‖|T| x‖ = ‖T x‖. This is the computational heart of the modulus API — the operator-norm and composition laws below all reduce to it.

@[simp]

theorem ContinuousLinearMap.modulus_apply_eq_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (x : E) : T.modulus x = 0 ↔ T x = 0

The modulus vanishes exactly where the operator does.

Immediate from norm_modulus_apply, but worth its own name: it is how the directed angle operators are shown to vanish off the source subspace.

@[simp]

theorem ContinuousLinearMap.norm_modulus {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : ‖T.modulus‖ = ‖T‖

The modulus has the same operator norm as the original map.

theorem ContinuousLinearMap.norm_modulus_comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (T : E →L[𝕜] F) (D : G →L[𝕜] E) : ‖T.modulus ∘SL D‖ = ‖T ∘SL D‖

Precomposition sees only the modulus: ‖|T| ∘L D‖ = ‖T ∘L D‖, since the two composites agree pointwise in norm.

theorem ContinuousLinearMap.norm_comp_modulus {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (D : E →L[𝕜] G) (T : E →L[𝕜] F) : ‖D ∘SL T.modulus‖ = ‖D ∘SL adjoint T‖

Postcomposition sees the modulus as the adjoint: ‖D ∘L |T|‖ = ‖D ∘L T⋆‖.

The two sides act on different spaces (|T| lives on the source of T, T⋆ on its target); the identity is between their operator norms, obtained by conjugating norm_modulus_comp with the isometric adjoint.

theorem ContinuousLinearMap.commute_modulus_of_commute_gram {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {b : E →L[𝕜] E} (h : Commute (adjoint T ∘SL T) b) : Commute T.modulus b

Anything commuting with the Gram operator T†T commutes with T.modulus.

theorem ContinuousLinearMap.modulus_commute_modulus {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] {S : E →L[𝕜] F} {T : E →L[𝕜] G} (h : Commute (adjoint S ∘SL S) (adjoint T ∘SL T)) : Commute S.modulus T.modulus

Moduli of operators whose Gram operators commute themselves commute. The two operators may have different targets: both moduli act on the common source space.

The endomorphism case

For T : E →L[𝕜] E the Gram operator is the C⋆-algebra element star T * T, so the modulus is the absolute value of T in the C⋆-algebra E →L[𝕜] E. These are specializations of the definition above, not a second construction.

theorem ContinuousLinearMap.commute_modulus_of_commute_star_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T b : E →L[𝕜] E) (h : Commute (star T * T) b) : Commute T.modulus b

Anything commuting with star T * T commutes with the modulus of the endomorphism T.

theorem ContinuousLinearMap.modulus_eq_sqrt_star_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : T.modulus = CFC.sqrt (star T * T)

On an endomorphism the modulus is the C⋆-algebra absolute value.

theorem ContinuousLinearMap.modulus_mul_self_eq_star_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : T.modulus * T.modulus = star T * T

The defining identity in C⋆-algebra form.