English
For a fixed a and subset s with quasispectrum ⊆ s, the map f ↦ cfcₙ(toFun { s } f) a is 1-Lipschitz on the f-continuous-on-s set.
Русский
Для фиксированного a и подмножества s с подмножество quasispectrum a ⊆ s отображение f ↦ cfcₙ(toFun { s } f) a является 1-Липшицевой на множество функций, непрерывных на s.
LaTeX
$$$a\\in A,\\; {s:Set R},\\; hs: quasispectrum R a \\subseteq s \Rightarrow \\ LipschitzOnWith 1 (\\lambda f. cfcₙ(toFun { s } f) a) {f | ContinuousOn (toFun { s } f) s}$$$
Lean4
/-- Let `s : Set 𝕜` be a compact set and consider pairs `(f, a) : (𝕜 → 𝕜) × A` where `f` is
continuous on `s`, maps zero itself, and `quasispectrum 𝕜 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 ∧ f 0 = 0} ×ˢ {a | p a ∧ quasispectrum 𝕜 a ⊆ s}) :=
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1 (fun f hf ↦ continuousOn_cfcₙ A hs ((toFun { s }) f) hf.1 hf.2)
(fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfcₙ_fun_of_subset a ha')
