Continuity of the functional calculus in its function at elements of finite spectrum #
Mathlib's tendsto_cfc_fun passes uniform convergence on the spectrum, among functions continuous
on the spectrum, to the continuous functional calculus. When the spectrum of a is finite, every
function is continuous on it and pointwise convergence on it is uniform, so pointwise convergence
on the spectrum alone gives cfc (F x) a → cfc f a. This applies, for example, to every matrix.
Main results #
TauCeti.tendsto_cfc_fun_of_finite_spectrum— at an element of finite spectrum, pointwise convergence of functions on the spectrum gives convergence of their functional calculi.
theorem
TauCeti.tendsto_cfc_fun_of_finite_spectrum
{X : Type u_1}
{R : Type u_2}
{A : Type u_3}
{p : A → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[IsTopologicalSemiring R]
[ContinuousStar R]
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra R A]
[ContinuousFunctionalCalculus R A p]
{l : Filter X}
{F : X → R → R}
{f : R → R}
{a : A}
(ha : (spectrum R a).Finite)
(hFf : ∀ t ∈ spectrum R a, Filter.Tendsto (fun (x : X) => F x t) l (nhds (f t)))
:
Filter.Tendsto (fun (x : X) => cfc (F x) a) l (nhds (cfc f a))
If the spectrum of a is finite and F x → f pointwise on it along a filter l, then
cfc (F x) a → cfc f a. No continuity of F x or f is needed.