The functional calculus of a symmetric operator in finite dimension

Let T be a symmetric endomorphism of a finite-dimensional inner product space E over ℝ or ℂ (any RCLike field 𝕜). For a real function f : ℝ → ℝ, the operator f(T) is the spectral sum ∑ᵢ f(λᵢ) eᵢ ⊗ eᵢ over an orthonormal eigenbasis (eᵢ) of T with eigenvalues (λᵢ). This file defines it as LinearMap.IsSymmetric.cfc and proves the identities that make it a functional calculus: f(T) acts as multiplication by f(λ) on every eigenvector of T with eigenvalue λ, and it is the unique endomorphism doing so. Everything else follows from this characterization: f(T) is symmetric, depends only on the values of f at the eigenvalues of T, is additive and multiplicative in f, recovers T from the identity function, is compatible with composition of functions, and is preserved by every linear map intertwining two symmetric operators. In particular f(T) commutes with every endomorphism commuting with T. A bound on |f| at the eigenvalues of T bounds the norm of f(T).

No continuity of f is required, and the construction works uniformly over RCLike scalars by finite sums, without any C⋆-algebra structure. It agrees with Mathlib's continuous functional calculus of the corresponding bounded operator: see LinearMap.IsSymmetric.toContinuousLinearMap_cfc. A function that is nonnegative at the eigenvalues of T gives a positive operator; applied to Real.sqrt on a positive operator, this yields the positive square root LinearMap.IsPositive.sqrt.

The name follows Matrix.IsHermitian.cfc, Mathlib's eigenbasis construction of the functional calculus of a Hermitian matrix.

Main declarations

• LinearMap.IsSymmetric.cfc: the functional calculus f(T) of a symmetric operator T.
• LinearMap.IsSymmetric.cfc_apply_of_apply_eq_smul: f(T)x = f(λ)x whenever Tx = λx.
• LinearMap.IsSymmetric.eq_cfc_iff: f(T) is the unique endomorphism acting by f(λ) on the eigenvectors of T with eigenvalue λ.
• LinearMap.IsSymmetric.cfc_eq_sum: the spectral sum formula over any ordered eigenbasis.
• LinearMap.IsSymmetric.isSymmetric_cfc, LinearMap.IsSymmetric.cfc_congr, LinearMap.IsSymmetric.cfc_id, LinearMap.IsSymmetric.cfc_mul, LinearMap.IsSymmetric.cfc_comp: the algebraic laws of the calculus.
• LinearMap.IsSymmetric.isPositive_cfc: f(T) is positive when f is nonnegative at the eigenvalues of T.
• LinearMap.IsSymmetric.comp_cfc_eq_cfc_comp and LinearMap.IsSymmetric.commute_cfc: intertwiners of symmetric operators intertwine their functional calculi; in particular the commutant of T commutes with f(T).
• LinearMap.IsSymmetric.norm_cfc_apply_le: ‖f(T)x‖ ≤ c‖x‖ when |f| ≤ c on the eigenvalues of T.
• LinearMap.IsSymmetric.norm_cfc_apply_sq_add_norm_cfc_apply_sq: ‖f(T)x‖² + ‖g(T)x‖² = ‖x‖² when f² + g² = 1 on the eigenvalues of T.

References

• R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), §§2.5 and 7.2 (the spectral theorem and functions of Hermitian matrices).

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

The functional calculus f(T) of a symmetric operator T on a finite-dimensional inner product space: the spectral sum ∑ᵢ f(λᵢ) eᵢ ⊗ eᵢ of the rank-one projections eᵢ ⊗ eᵢ = rankOne 𝕜 eᵢ eᵢ over Mathlib's ordered orthonormal eigenbasis (eᵢ) of T, whose eigenvalues are (λᵢ).

The result does not depend on the choice of eigenbasis: see cfc_eq_sum and eq_cfc_iff.

theorem LinearMap.IsSymmetric.cfc_apply_of_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) {x : E} {μ : ℝ} (hx : T x = ↑μ • x) : (hT.cfc f) x = ↑(f μ) • x

Eigenvector action. If Tx = μx, then f(T)x = f(μ)x.

@[simp]

theorem LinearMap.IsSymmetric.cfc_apply_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (f : ℝ → ℝ) (i : Fin n) : (hT.cfc f) ((hT.eigenvectorBasis hn) i) = ↑(f (hT.eigenvalues hn i)) • (hT.eigenvectorBasis hn) i

The functional calculus acts diagonally on every ordered eigenbasis of T.

theorem LinearMap.IsSymmetric.eq_cfc_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) {S : E →ₗ[𝕜] E} : S = hT.cfc f ↔ ∀ (μ : ℝ) (x : E), T x = ↑μ • x → S x = ↑(f μ) • x

Uniqueness. An endomorphism equals f(T) exactly when it acts as multiplication by f(μ) on every eigenvector of T with eigenvalue μ.

theorem LinearMap.IsSymmetric.cfc_eq_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (f : ℝ → ℝ) : hT.cfc f = ∑ i : Fin n, ↑(f (hT.eigenvalues hn i)) • ↑(((InnerProductSpace.rankOne 𝕜) ((hT.eigenvectorBasis hn) i)) ((hT.eigenvectorBasis hn) i))

The functional calculus is the spectral sum over any ordered eigenbasis of T.

theorem LinearMap.IsSymmetric.cfc_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (f : ℝ → ℝ) (x : E) : (hT.cfc f) x = ∑ i : Fin n, (↑(f (hT.eigenvalues hn i)) * inner 𝕜 ((hT.eigenvectorBasis hn) i) x) • (hT.eigenvectorBasis hn) i

The spectral expansion of f(T)x in any ordered eigenbasis of T.

theorem LinearMap.IsSymmetric.isSymmetric_cfc {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) : (hT.cfc f).IsSymmetric

The functional calculus of a symmetric operator is symmetric.

theorem LinearMap.IsSymmetric.cfc_congr {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {f g : ℝ → ℝ} (hfg : ∀ (μ : ℝ), Module.End.HasEigenvalue T ↑μ → f μ = g μ) : hT.cfc f = hT.cfc g

The functional calculus only depends on the values of f at the eigenvalues of T.

@[simp]

theorem LinearMap.IsSymmetric.cfc_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : hT.cfc _root_.id = T

The identity function recovers the operator.

@[simp]

theorem LinearMap.IsSymmetric.cfc_id' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (hT.cfc fun (μ : ℝ) => μ) = T

The identity function, written as a lambda, recovers the operator.

@[simp]

theorem LinearMap.IsSymmetric.cfc_const {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (c : ℝ) : (hT.cfc fun (x : ℝ) => c) = ↑c • 1

A constant function gives the corresponding multiple of the identity.

@[simp]

theorem LinearMap.IsSymmetric.cfc_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : hT.cfc 0 = 0

The zero function gives the zero operator.

@[simp]

theorem LinearMap.IsSymmetric.cfc_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : hT.cfc 1 = 1

The constant function 1 gives the identity operator.

theorem LinearMap.IsSymmetric.cfc_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f g : ℝ → ℝ) : hT.cfc (f + g) = hT.cfc f + hT.cfc g

The functional calculus is additive in the function.

theorem LinearMap.IsSymmetric.cfc_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f g : ℝ → ℝ) : hT.cfc (f * g) = hT.cfc f * hT.cfc g

Product law. The functional calculus is multiplicative in the function: (fg)(T) = f(T)g(T).

theorem LinearMap.IsSymmetric.cfc_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f g : ℝ → ℝ) : hT.cfc (g ∘ f) = ⋯.cfc g

Composition of functions corresponds to iterating the functional calculus: (g ∘ f)(T) = g(f(T)).

theorem LinearMap.IsSymmetric.comp_cfc_eq_cfc_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {T' : F →ₗ[𝕜] F} (hT' : T'.IsSymmetric) {S : E →ₗ[𝕜] F} (hS : S ∘ₗ T = T' ∘ₗ S) (f : ℝ → ℝ) : S ∘ₗ hT.cfc f = hT'.cfc f ∘ₗ S

A linear map intertwining two symmetric operators intertwines their functional calculi: if S T = T' S, then S f(T) = f(T') S.

theorem LinearMap.IsSymmetric.commute_cfc {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {S : E →ₗ[𝕜] E} (hS : Commute S T) (f : ℝ → ℝ) : Commute S (hT.cfc f)

Commutant preservation. Every endomorphism commuting with T commutes with f(T).

theorem LinearMap.IsSymmetric.norm_cfc_apply_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) {c : ℝ} (hf : ∀ (μ : ℝ), Module.End.HasEigenvalue T ↑μ → |f μ| ≤ c) (x : E) : ‖(hT.cfc f) x‖ ≤ c * ‖x‖

Norm bound. If |f(λ)| ≤ c at every eigenvalue λ of T, then ‖f(T)x‖ ≤ c‖x‖.

theorem LinearMap.IsSymmetric.norm_cfc_apply_sq_add_norm_cfc_apply_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {f g : ℝ → ℝ} (hfg : ∀ (μ : ℝ), Module.End.HasEigenvalue T ↑μ → f μ ^ 2 + g μ ^ 2 = 1) (x : E) : ‖(hT.cfc f) x‖ ^ 2 + ‖(hT.cfc g) x‖ ^ 2 = ‖x‖ ^ 2

Pythagorean splitting. If f(λ)² + g(λ)² = 1 at every eigenvalue λ of T, then ‖f(T)x‖² + ‖g(T)x‖² = ‖x‖². For instance f = sin and g = cos.

theorem LinearMap.IsSymmetric.isPositive_cfc {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {f : ℝ → ℝ} (hf : ∀ (μ : ℝ), Module.End.HasEigenvalue T ↑μ → 0 ≤ f μ) : (hT.cfc f).IsPositive

Positivity. If f is nonnegative at every eigenvalue of T, then f(T) is positive.