The continuous functional calculus of an element with finite spectrum

If the spectrum of a is finite, every scalar function is continuous on it, so cfc f a is the genuine functional calculus of a for every f. For a point μ, the difference quotient g x = (f x - f μ) / (x - μ) is then also an admissible symbol, and the scalar identity f x = g x (x - μ) + f μ (valid at x = μ as well, since division by zero is zero) passes to the calculus:

cfc f a - f(μ) = cfc g a * (a - μ).

Consequently cfc f a acts as multiplication by f μ on every eigenvector of a for the eigenvalue μ, in any module over the algebra. This is the description of the functional calculus through eigenvectors, which is exact in finite dimension: the main examples of elements with finite spectrum are the bounded operators on a finite-dimensional normed space, whose spectrum is finite over every field of scalars acting compatibly (ContinuousLinearMap.finite_spectrum). There the eigenvector action identifies the continuous functional calculus with any spectral construction acting by f μ on the eigenvectors for μ.

When the spectrum lies in a finite set s, the functional calculus is Lagrange interpolation on the nodes s: cfc f a = ∑ μ ∈ s, f μ • ℓ_μ(a), where ℓ_μ is the Lagrange basis polynomial that is 1 at μ and 0 at the other nodes. The elements ℓ_μ(a) do not depend on f, so every cfc f a is a fixed linear combination of polynomials in a, with coefficients the values of f.

Main results

• TauCeti.cfc_sub_algebraMap_eq_mul: cfc f a - f(μ) = cfc g a * (a - μ) for the difference quotient g of f at μ.
• TauCeti.cfc_smul_of_smul_eq_algebraMap_smul: if a • m = μ • m, then cfc f a • m = f(μ) • m.
• TauCeti.cfc_eq_sum_smul_aeval_lagrangeBasis: if the spectrum of a lies in the finite set s, then cfc f a = ∑ μ ∈ s, f μ • ℓ_μ(a) for the Lagrange basis polynomials ℓ_μ of s.

theorem TauCeti.cfc_sub_algebraMap_eq_mul {R : Type u_1} {A : Type u_2} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f : R → R) {a : A} (hfin : (spectrum R a).Finite) (μ : R) (ha : p a := by cfc_tac) : cfc f a - (algebraMap R A) (f μ) = cfc (fun (x : R) => (f x - f μ) / (x - μ)) a * (a - (algebraMap R A) μ)

Factoring out an eigenvalue. For an element a with finite spectrum and any point μ, cfc f a - f(μ) factors through a - μ via the difference quotient of f at μ. No continuity of f is needed, since every function is continuous on a finite set.

theorem TauCeti.cfc_smul_of_smul_eq_algebraMap_smul {R : Type u_1} {A : Type u_2} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] {M : Type u_3} [AddCommGroup M] [Module A M] (f : R → R) {a : A} (hfin : (spectrum R a).Finite) {μ : R} {m : M} (hm : a • m = (algebraMap R A) μ • m) (ha : p a := by cfc_tac) : cfc f a • m = (algebraMap R A) (f μ) • m

Eigenvector action. If a has finite spectrum and a • m = μ • m in a module over the algebra, then cfc f a • m = f(μ) • m for every scalar function f.

theorem TauCeti.cfc_eq_sum_smul_aeval_lagrangeBasis {R : Type u_1} {A : Type u_2} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [DecidableEq R] (f : R → R) {a : A} {s : Finset R} (hs : spectrum R a ⊆ ↑s) (ha : p a := by cfc_tac) : cfc f a = ∑ μ ∈ s, f μ • (Polynomial.aeval a) (Lagrange.basis s id μ)

The functional calculus as Lagrange interpolation. If the spectrum of a lies in the finite set s, then cfc f a = ∑ μ ∈ s, f μ • ℓ_μ(a), where ℓ_μ = Lagrange.basis s id μ is the Lagrange basis polynomial of the nodes s that is 1 at μ and 0 at the other nodes.