The finite symmetric calculus and modulus agree with the continuous functional calculus

On a finite-dimensional inner product space E over 𝕜 = ℝ or ℂ, there are two functional calculi for a symmetric operator T: the spectral sum LinearMap.IsSymmetric.cfc, defined for every real function through an orthonormal eigenbasis, and Mathlib's continuous functional calculus cfc f T of the self-adjoint bounded operator T. Likewise there are two square roots of a positive operator and two moduli √(A† A) of a linear map. This file proves that the two constructions coincide after the identification LinearMap.toContinuousLinearMap of linear maps with bounded operators, so that results proved for either can be used for both.

The comparison rests on the eigenvector description of the continuous functional calculus. The spectrum of a finite-dimensional operator is finite, so cfc f T acts on every eigenvector of T for the eigenvalue μ as multiplication by f μ (TauCeti.cfc_smul_of_smul_eq_algebraMap_smul), which characterizes the spectral sum (LinearMap.IsSymmetric.eq_cfc_iff). In particular no continuity of f is needed.

The statements are uniform in the scalar field. They assume a real algebra structure on E →L[𝕜] E compatible with the 𝕜-scalars and a continuous functional calculus over ℝ for self-adjoint operators, the setting of Mathlib's star order on bounded operators (Mathlib.Analysis.InnerProductSpace.StarOrder); the square-root statements also assume that this order makes E →L[𝕜] E a star-ordered ring. At 𝕜 = ℂ all of this is Mathlib's structure on the complex C⋆-algebra E →L[ℂ] E, and at 𝕜 = ℝ it is supplied by ContinuousLinearMap.instContinuousFunctionalCalculusRealIsSelfAdjoint. Completeness of E, automatic in finite dimension, is assumed because Mathlib's adjoint on E →L[𝕜] E requires it.

Main results

• ContinuousLinearMap.cfc_apply_of_apply_eq_smul: if T x = μ x, then f(T) x = f(μ) x.
• LinearMap.IsSymmetric.toContinuousLinearMap_cfc: the finite spectral calculus f(T) is the continuous functional calculus cfc f T.
• ContinuousLinearMap.cfc_indicator_eq_starProjection: the spectral projector cfc (Ω.indicator 1) T of a self-adjoint T is the orthogonal projection onto the point-spectral subspace Module.End.pointSpectralSubspace T Ω.
• LinearMap.IsPositive.toContinuousLinearMap_sqrt: the finite positive square root is CFC.sqrt.
• LinearMap.toContinuousLinearMap_operatorAbs: the finite modulus of a rectangular map A is the square root CFC.sqrt (A† A) of its source Gram operator.
• LinearMap.toContinuousLinearMap_operatorAbs_eq_cfcAbs: the finite modulus of an endomorphism is its absolute value CFC.abs in the C⋆-algebra sense.
• LinearMap.toContinuousLinearMap_operatorAbs_eq_modulus: the finite and bounded modulus constructions coincide for every finite-dimensional real or complex inner product space.

theorem ContinuousLinearMap.cfc_apply_of_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] (f : ℝ → ℝ) {T : E →L[𝕜] E} {x : E} {μ : ℝ} (hx : T x = ↑μ • x) (hT : IsSelfAdjoint T := by cfc_tac) : (cfc f T) x = ↑(f μ) • x

Eigenvector action of the continuous functional calculus. On a finite-dimensional space, if a self-adjoint operator T satisfies T x = μ x, then f(T) x = f(μ) x for every real function f.

theorem LinearMap.IsSymmetric.toContinuousLinearMap_cfc {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) : toContinuousLinearMap (hT.cfc f) = _root_.cfc f (toContinuousLinearMap T)

Agreement of the finite and continuous functional calculi. For a symmetric operator T on a finite-dimensional space and any real function f, the spectral sum f(T) is the continuous functional calculus cfc f T of T viewed as a bounded operator.

theorem LinearMap.IsPositive.toContinuousLinearMap_sqrt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] [StarOrderedRing (E →L[𝕜] E)] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : toContinuousLinearMap hT.sqrt = CFC.sqrt (toContinuousLinearMap T)

The finite positive square root of a positive operator is the continuous-functional-calculus square root CFC.sqrt.

theorem LinearMap.toContinuousLinearMap_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] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] [StarOrderedRing (E →L[𝕜] E)] (A : E →ₗ[𝕜] F) : toContinuousLinearMap A.operatorAbs = CFC.sqrt (toContinuousLinearMap (adjoint A) ∘SL toContinuousLinearMap A)

The finite modulus |A| of a rectangular linear map A is the continuous-functional-calculus square root of the source Gram operator A† A.

theorem LinearMap.toContinuousLinearMap_operatorAbs_eq_cfcAbs {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] [StarOrderedRing (E →L[𝕜] E)] (A : E →ₗ[𝕜] E) : toContinuousLinearMap A.operatorAbs = CFC.abs (toContinuousLinearMap A)

The finite modulus is the absolute value. For an endomorphism A of a finite-dimensional space, the finite modulus |A| = √(A† A) is the absolute value CFC.abs A of A in the bounded operators.

theorem LinearMap.toContinuousLinearMap_operatorAbs_eq_modulus {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] [StarOrderedRing (E →L[𝕜] E)] [CompleteSpace F] (A : E →ₗ[𝕜] F) : toContinuousLinearMap A.operatorAbs = (toContinuousLinearMap A).modulus

Agreement of the finite and bounded moduli. For a linear map between finite-dimensional real or complex inner product spaces, the finite spectral modulus is the bounded-operator modulus after converting the maps to continuous linear maps.

theorem ContinuousLinearMap.cfc_indicator_eq_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint] (Ω : Set ℝ) {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) : cfc (Ω.indicator 1) T = (Module.End.pointSpectralSubspace (↑T) Ω).starProjection

The spectral projector is an orthogonal projection. For a self-adjoint operator T on a finite-dimensional space and a set Ω ⊆ ℝ, cfc (Ω.indicator 1) T is the orthogonal projection onto the sum of the eigenspaces of T at the eigenvalues in Ω.