English
If F tends uniformly to f on the spectrum of a and each F x is continuous on that spectrum, then x ↦ cfc(F x) a tends to cfc f a.
Русский
Если F стремится равномерно к f на спектре a и каждый F x непрерывен на спектре, то x ↦ cfc(F x) a сходится к cfc f a.
LaTeX
$$$\\text{TendstoUniformlyOn } F \\ f\\ l (\\text{spectrum } R a) \\land (\\forall x, ContinuousOn(Fx, \\text{spectrum } R a)) \\Rightarrow \\ Tendsto(x \\mapsto cfc(Fx) a)\\ l\\ (\\ nhds (cfc f a))$$$
Lean4
/-- If `F : X → R → R` tends to `f : R → R` uniformly on the spectrum of `a`, and all
these functions are continuous on the spectrum, then `fun x ↦ cfc (F x) a` tends
to `cfc f a`. -/
theorem tendsto_cfc_fun {l : Filter X} {F : X → R → R} {f : R → R} {a : A}
(h_tendsto : TendstoUniformlyOn F f l (spectrum R a)) (hF : ∀ᶠ x in l, ContinuousOn (F x) (spectrum R a)) :
Tendsto (fun x ↦ cfc (F x) a) l (𝓝 (cfc f a)) := by
open scoped ContinuousFunctionalCalculus in
obtain (rfl | hl) := l.eq_or_neBot
· simp
have hf := h_tendsto.continuousOn hF
by_cases ha : p a
· let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
conv =>
enter [1, x]
rw [Function.comp_apply, cfc_apply (hf := x.2)]
rw [cfc_apply ..]
apply cfcHom_continuous _ |>.tendsto _ |>.comp
rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
intro t
simp only [eventually_comap, Subtype.forall]
peel h_tendsto t with ht x _
simp_all
· simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds
