English
If TendstoUniformlyOn F f l (quasispectrum R a), and hF: ∀ᶠ x in l, ContinuousOn (F x) (quasispectrum R a), then Tendsto (x ↦ cfcₙ (F x) a) l (nhds (cfcₙ f a)).
Русский
Если F сходится равномерно к f в спектре quasispectrum и каждое F x непрерывно на спектре, то cfcₙ(F x) a сходится к cfcₙ f a.
LaTeX
$$$\\text{TendstoUniformlyOn } F f l (\\text{quasispectrum } R a) \\rightarrow (\\forallᶠ x \\in l, ContinuousOn (F x) (\\text{quasispectrum } R a)) \\rightarrow \\ Tendsto (x \\mapsto cfcₙ (F x) a) l (nhds (cfcₙ f a))$$$
Lean4
/-- Let `s : Set 𝕜` be a compact set and consider pairs `(f, a) : (𝕜 → 𝕜) × A` where `f` is
continuous on `s` and `spectrum 𝕜 a ⊆ s` and `a` satisfies the predicate `p a` for the continuous
functional calculus.
Then `cfc` is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on `s`. -/
theorem continuousOn_cfc_setProd {s : Set 𝕜} (hs : IsCompact s) :
ContinuousOn (fun fa : (𝕜 →ᵤ[{ s }] 𝕜) × A ↦ cfc (toFun { s } fa.1) fa.2)
({f | ContinuousOn (toFun { s } f) s} ×ˢ {a | p a ∧ spectrum 𝕜 a ⊆ s}) :=
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1 (fun f hf ↦ continuousOn_cfc A hs ((toFun { s }) f) hf)
(fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfc_fun_of_subset a ha')
