Finite-dimensional self-adjoint functional calculus

For a symmetric endomorphism on a finite-dimensional real or complex inner-product space, apply a real scalar function to the ordered eigenvalues and reconstruct the operator in the associated orthonormal eigenbasis.

The construction is intended as a small RCLike counterpart of the continuous functional calculus. It is sufficient for functions such as arcsin and the totalized tangent functions used by finite-dimensional operator-angle theory.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.SelfAdjointFunctionalCalculus, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit caa0966.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

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

Apply a real function to the spectrum of a finite-dimensional symmetric endomorphism.

Equations

• One or more equations did not get rendered due to their size.

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

The calculus is additive in the symbol: a finite sum of rank-one terms, added coefficientwise.

theorem TauCeti.selfAdjointFunctionalCalculus_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (c : ℝ) (f : ℝ → ℝ) : selfAdjointFunctionalCalculus hT (c • f) = ↑c • selfAdjointFunctionalCalculus hT f

The calculus is real-homogeneous in the symbol.

theorem TauCeti.selfAdjointFunctionalCalculus_apply_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) (k : Fin (Module.finrank 𝕜 E)) : (selfAdjointFunctionalCalculus hT f) ((hT.eigenvectorBasis ⋯) k) = ↑(f (hT.eigenvalues ⋯ k)) • (hT.eigenvectorBasis ⋯) k

The functional calculus acts diagonally in the chosen eigenbasis.

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

Applying a real function to a symmetric operator remains symmetric.

theorem TauCeti.selfAdjointFunctionalCalculus_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {f : ℝ → ℝ} (hf : ∀ (i : Fin (Module.finrank 𝕜 E)), 0 ≤ f (hT.eigenvalues ⋯ i)) : (selfAdjointFunctionalCalculus hT f).IsPositive

A symbol nonnegative on the spectrum gives a positive operator.

Each rank-one summand is positive, and the coefficient f (λᵢ) scales it by a nonnegative real. Only the values at the eigenvalues matter, so the hypothesis is stated there rather than on all of ℝ.

theorem TauCeti.norm_selfAdjointFunctionalCalculus_apply_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ (i : Fin (Module.finrank 𝕜 E)), |f (hT.eigenvalues ⋯ i)| ≤ M) (x : E) : ‖(selfAdjointFunctionalCalculus hT f) x‖ ≤ M * ‖x‖

The calculus is bounded by the sup of the symbol on the spectrum.

Parseval in the eigenbasis: the calculus multiplies the i-th coordinate of x by f (λᵢ), so the squared norm is a weighted sum of the coordinate weights. This is the estimate continuity of f ↦ calculus hT f rests on.

theorem TauCeti.selfAdjointFunctionalCalculus_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : selfAdjointFunctionalCalculus hT id = T

The identity function recovers the original symmetric operator.

theorem TauCeti.selfAdjointFunctionalCalculus_congr_op {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (h : T = S) (f : ℝ → ℝ) : selfAdjointFunctionalCalculus hT f = selfAdjointFunctionalCalculus hS f

The calculus depends only on the operator, not on the symmetry witness. The operator occurs solely inside that witness's type, so a plain rewrite cannot reach it; this is the bridge that lets callers replace it.

theorem TauCeti.selfAdjointFunctionalCalculus_congr {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {f g : ℝ → ℝ} (hfg : ∀ (i : Fin (Module.finrank 𝕜 E)), f (hT.eigenvalues ⋯ i) = g (hT.eigenvalues ⋯ i)) : selfAdjointFunctionalCalculus hT f = selfAdjointFunctionalCalculus hT g

Functions agreeing on every eigenvalue produce the same operator.

theorem TauCeti.selfAdjointFunctionalCalculus_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f g : ℝ → ℝ) : selfAdjointFunctionalCalculus hT f ∘ₗ selfAdjointFunctionalCalculus hT g = selfAdjointFunctionalCalculus hT fun (x : ℝ) => f x * g x

Composition corresponds to pointwise multiplication of scalar functions.

@[simp]

theorem TauCeti.selfAdjointFunctionalCalculus_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (selfAdjointFunctionalCalculus hT fun (x : ℝ) => 0) = 0

Constant zero gives the zero operator.

theorem TauCeti.selfAdjointFunctionalCalculus_real_smul_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (r : ℝ) (f : ℝ → ℝ) : have hS := ⋯; selfAdjointFunctionalCalculus hS f = ↑(f r) • LinearMap.id

Functional calculus of a real scalar multiple of the identity is scalar evaluation. This is the finite RCLike bridge used by planar angle models.

theorem TauCeti.selfAdjointFunctionalCalculus_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} {lam : ℝ} (hx : T x = ↑lam • x) : (selfAdjointFunctionalCalculus hT f) x = ↑(f lam) • x

Functional calculus on an arbitrary eigenvector. Unlike the basis lemma, this form is stable on repeated eigenspaces and is the key commutant property.

theorem TauCeti.selfAdjointFunctionalCalculus_intertwines {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) {B : F →ₗ[𝕜] F} (hB : B.IsSymmetric) (J : E →ₗ[𝕜] F) (hJ : J ∘ₗ A = B ∘ₗ J) (f : ℝ → ℝ) : J ∘ₗ selfAdjointFunctionalCalculus hA f = selfAdjointFunctionalCalculus hB f ∘ₗ J

Finite self-adjoint functional calculus preserves intertwiners.

If J A = B J for symmetric finite-dimensional operators, then applying the same real scalar function to both spectra preserves that relation. The proof uses an eigenbasis of A: intertwining sends each basis vector either to zero or to a B-eigenvector with the same eigenvalue, and the functional calculus therefore acts by the same scalar on both sides.

This is the finite RCLike counterpart of the continuous-functional-calculus intertwiner used by the infinite-dimensional theory.

theorem TauCeti.repr_eq_zero_of_calculus_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} {lam : ℝ} (hx : (selfAdjointFunctionalCalculus hT f) x = ↑lam • x) {i : Fin (Module.finrank 𝕜 E)} (hi : f (hT.eigenvalues ⋯ i) ≠ lam) : ((hT.eigenvectorBasis ⋯).repr x).ofLp i = 0

An eigenvector of f(T) is blind to the eigenvalues f does not send to its eigenvalue.

If f(T) x = lam • x, then x has no component along an eigenvector of T whose eigenvalue f moves away from lam. This is the one computation behind both transfer lemmas below, and it is selfAdjointFunctionalCalculus_isSymmetric applied to the pair (f(T) (b i), f(T) x).

theorem TauCeti.selfAdjointFunctionalCalculus_apply_of_calculus_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f g : ℝ → ℝ) {x : E} {lam mu : ℝ} (hx : (selfAdjointFunctionalCalculus hT f) x = ↑lam • x) (hfg : ∀ (i : Fin (Module.finrank 𝕜 E)), f (hT.eigenvalues ⋯ i) = lam → g (hT.eigenvalues ⋯ i) = mu) : (selfAdjointFunctionalCalculus hT g) x = ↑mu • x

Transfer of an eigenvector between two symbols of the same operator.

If f(T) scales x by lam, and a second symbol g takes the constant value mu at every eigenvalue that f sends to lam, then g(T) scales x by mu. Taking f = id recovers selfAdjointFunctionalCalculus_apply_of_apply_eq_smul.

This is what lets an eigenvector of an operator that is defined as a functional calculus — an operator angle Θ = arcsin (sin Θ), say — be pushed through a different symbol without ever naming the eigenbasis.

theorem TauCeti.exists_eigenvalue_of_calculus_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} {lam : ℝ} (hx0 : x ≠ 0) (hx : (selfAdjointFunctionalCalculus hT f) x = ↑lam • x) : ∃ (i : Fin (Module.finrank 𝕜 E)), f (hT.eigenvalues ⋯ i) = lam

A nonzero eigenvector of f(T) exhibits its eigenvalue as a value of f.

Contrapositive of repr_eq_zero_of_calculus_apply_eq_smul: if f missed lam at every eigenvalue of T, then every coordinate of x in the eigenbasis would vanish. This is what pins the range of an operator angle: an eigenvalue of arcsin (sin Θ) is an actual arcsine, hence lies in [-π/2, π/2].

theorem TauCeti.selfAdjointFunctionalCalculus_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (selfAdjointFunctionalCalculus hT fun (x : ℝ) => 1) = LinearMap.id

The constant function 1 gives the identity operator.

theorem TauCeti.selfAdjointFunctionalCalculus_pow {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (n : ℕ) : (selfAdjointFunctionalCalculus hT fun (x : ℝ) => x ^ n) = T ^ n

The calculus agrees with polynomial evaluation on monomials.

Induction on n from ..._one and ..._comp; the base is the identity operator and the step is multiplicativity of the symbol. This is what makes the calculus an algebra map extending Polynomial.aeval, the property any route to the Mathlib CFC goes through.

theorem TauCeti.selfAdjointFunctionalCalculus_indicator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {S : Set ℝ} (hS : ∀ (i : Fin (Module.finrank 𝕜 E)), hT.eigenvalues ⋯ i ∈ S) (g : ℝ → ℝ) : selfAdjointFunctionalCalculus hT (S.indicator g) = selfAdjointFunctionalCalculus hT g

Extending a symbol by zero off a set containing the spectrum changes nothing.

The calculus sees f only at the eigenvalues, so restricting a symbol to any set containing them and extending by zero leaves the operator alone. This is what lets a g : C(spectrum ℝ a, ℝ) be turned into an ℝ → ℝ for the finite calculus without the algebra operations drifting: indicator commutes with + and *, and the mismatch at 1 is invisible here.

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

Multiplicativity in pointwise-product form, the shape an algebra map needs.

selfAdjointFunctionalCalculus_comp states this with an explicit lambda. f * g on ℝ → ℝ is that lambda definitionally, but rw matches syntactically and Lean normalises the lambda to *, so the algebra-map fields need this spelling.

noncomputable def TauCeti.extendSymbol {S : Set ℝ} (g : C(↑S, ℝ)) : ℝ → ℝ

Extend a continuous function on a subset of ℝ to all of ℝ by zero.

The finite calculus consumes ℝ → ℝ, while cfcHom is stated on C(spectrum ℝ a, ℝ); this is the bridge between the two. It is multiplicative and additive outright — both sides vanish off S — and selfAdjointFunctionalCalculus_indicator covers the unit, the one operation it does not respect.

Equations

• TauCeti.extendSymbol g x = if h : x ∈ S then g ⟨x, h⟩ else 0

@[simp]

theorem TauCeti.extendSymbol_apply_of_mem {S : Set ℝ} (g : C(↑S, ℝ)) {x : ℝ} (hx : x ∈ S) : extendSymbol g x = g ⟨x, hx⟩

On S the extension by zero agrees with the symbol.

@[simp]

theorem TauCeti.extendSymbol_apply_of_not_mem {S : Set ℝ} (g : C(↑S, ℝ)) {x : ℝ} (hx : x ∉ S) : extendSymbol g x = 0

Off S the extension is zero. With extendSymbol_apply_of_mem this determines extendSymbol pointwise, so a consumer never has to reduce through the body.

theorem TauCeti.extendSymbol_eq_indicator {S : Set ℝ} (g : C(↑S, ℝ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ) (hx : x ∈ S), f x = g ⟨x, hx⟩) : extendSymbol g = S.indicator f

extendSymbol as a set indicator, the form the calculus bridge consumes.

theorem TauCeti.extendSymbol_mul {S : Set ℝ} (g₁ g₂ : C(↑S, ℝ)) : extendSymbol (g₁ * g₂) = fun (x : ℝ) => extendSymbol g₁ x * extendSymbol g₂ x

Extension by zero is multiplicative: both sides vanish off S.

theorem TauCeti.extendSymbol_add {S : Set ℝ} (g₁ g₂ : C(↑S, ℝ)) : extendSymbol (g₁ + g₂) = extendSymbol g₁ + extendSymbol g₂

Extension by zero is additive.

@[simp]

theorem TauCeti.extendSymbol_zero {S : Set ℝ} : extendSymbol 0 = fun (x : ℝ) => 0

Extension by zero sends the zero symbol to the zero function.

theorem TauCeti.extendSymbol_one_eq_indicator {S : Set ℝ} : extendSymbol 1 = S.indicator fun (x : ℝ) => 1

The extension of the constant symbol 1 is the indicator of S -- not the constant function 1, which is why extension by zero is not unital.

theorem TauCeti.selfAdjointFunctionalCalculus_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T B : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (f : ℝ → ℝ) (hBT : B ∘ₗ T = T ∘ₗ B) : B ∘ₗ selfAdjointFunctionalCalculus hT f = selfAdjointFunctionalCalculus hT f ∘ₗ B

Every operator commuting with a symmetric map commutes with its finite real functional calculus. This includes repeated eigenvalues: the proof uses that the commuting operator preserves each eigenspace.

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

Spectral positive square root of a positive symmetric operator T, as the functional calculus of Real.sqrt: sqrt T = ∑ᵢ √λᵢ • (rank-one projection onto the i-th eigenvector), where λᵢ ≥ 0 are the eigenvalues of T. Source: Horn--Johnson Thm 7.2.6.

This was once a second noncomputable def with that sum written out, and the library proved the two coincide by rfl — one object defined twice. The duplicate has been collapsed; the uniqueness theory that only the square root has (sqrt_unique, ker_sqrt, range_sqrt, sqrt_mul_self) is unchanged and still lives in ForTauCeti/Analysis/InnerProductSpace/PositiveSqrt.lean, which now imports this module rather than the other way round.

Equations

• hT.sqrt = TauCeti.selfAdjointFunctionalCalculus ⋯ Real.sqrt

theorem TauCeti.selfAdjointFunctionalCalculus_sqrt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : selfAdjointFunctionalCalculus ⋯ Real.sqrt = hT.sqrt

The spectral square root is the finite self-adjoint functional calculus of Real.sqrt. True by definition; kept because it is the name downstream proofs rewrite with.

theorem TauCeti.sqrt_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T B : E →ₗ[𝕜] E} (hT : T.IsPositive) (hBT : B ∘ₗ T = T ∘ₗ B) : B ∘ₗ hT.sqrt = hT.sqrt ∘ₗ B

Commutation passes from a positive operator to its positive square root.