English
Let s be a compact subset of NNReal. Consider pairs (f, a) where f is continuous on s, f(0) = 0, the spectrum of a satisfies spectrum_ℝ≥0(a) ⊆ s, and a ≥ 0. Then the nonunital continuous functional calculus cfcₙ is jointly continuous in (f, a) when the function space is endowed with the topology of uniform convergence on s.
Русский
Пусть s — компактное множество в NNReal. Рассмотрим пары (f, a), где f непрерывна на s, f(0) = 0, спектр a удовлетворяет spectrumℝ≥0(a) ⊆ s и a ≥ 0. Тогда cfcₙ непрерывно зависит от обеих переменных вместе, если пространство функций оснащено топологией равномерной сходимости на s.
LaTeX
$$$$\\operatorname{ContinuousOn}\\left(\\lambda fa : (\\mathbb{R}_{\\ge 0} \\to\\!\\mathrm{unif}\\!{s}\\ \\mathbb{R}_{\\ge 0}) \\times A \\mapsto cfc_n\\bigl(\\operatorname{toFun} { s } fa.1\\bigr) fa.2\\right)\\left(\\{f \\mid \\operatorname{ContinuousOn}(\\operatorname{toFun} { s } f) s \\land f(0)=0\\} \\times\\!^{\\mathrm{S}} \\{a \\mid 0 \\le a \\land \\operatorname{quasispectrum} \\mathbb{R}_{\\ge 0} a \\subseteq s\\}\\right)$$$$
Lean4
/-- Let `s : Set ℝ≥0` be a compact set and consider pairs `(f, a) : (ℝ≥0 → ℝ≥0) × A` where `f` is
continuous on `s`, maps zero to itself, `spectrum ℝ≥0 a ⊆ s` and `0 ≤ a`.
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ₙ_nnreal_setProd {s : Set ℝ≥0} (hs : IsCompact s) :
ContinuousOn (fun fa : (ℝ≥0 →ᵤ[{ s }] ℝ≥0) × A ↦ cfcₙ (toFun { s } fa.1) fa.2)
({f | ContinuousOn (toFun { s } f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}) :=
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1
(fun f hf ↦ continuousOn_cfcₙ_nnreal A hs ((toFun { s }) f) hf.1 hf.2)
(fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfcₙ_fun_of_subset a ha')
