English
For f with SpectrumRestricts a f, and any g: R → R, the functional calculus after applying g is the same as applying g after mapping through the base embedding; i.e., cfc g a = cfc (algebraMap R S ∘ g ∘ f) a.
Русский
Пусть $f$ удовлетворяет SpectrumRestricts на $a$. Для любого $g:R\\to R$ вычисление через $g$ на $a$ эквивалентно вычислению через композицию $\\mathrm{algebraMap}(R,S)\\circ g\\circ f$: \\(\\mathrm{cfc}\,g\,a = \\mathrm{cfc}(\\lambda x. \\mathrm{algebraMap}_{R S}(g(f(x))))\,a.\\)
LaTeX
$$$\\forall g:R\\to R,\\; \\mathrm{cfc}\\,g\\,a = \\mathrm{cfc}\\left(\\lambda x. \\mathrm{algebraMap}(R,S)(g(f(x)))\\right) a$$$
Lean4
theorem cfc_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a)
(h : SpectrumRestricts a f) (g : R → R) : cfc g a = cfc (fun x ↦ algebraMap R S (g (f x))) a :=
by
by_cases hg : ContinuousOn g (spectrum R a)
· rw [cfc_apply g a, cfcHom_eq_restrict f halg hpa hqa h, SpectrumRestricts.starAlgHom_apply, cfcHom_eq_cfc_extend 0]
apply cfc_congr fun x hx ↦ ?_
lift x to spectrum S a using hx
simp [Function.comp]
· have : ¬ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (spectrum S a) :=
by
refine fun hg' ↦ hg ?_
rw [halg.isEmbedding.continuousOn_iff]
simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this]
