English
If s is compact and a satisfies 0 ≤ a and spectrum ⊆ s, then the map (f,a) ↦ cfc(toFun{ s } f) a is jointly continuous on the product of continuous-on f and spectral subset constraints.
Русский
Если s компактно и 0 ≤ a, спектр ⊆ s, то отображение пары (f,a) ↦ cfc(toFun{s} f) a непрерывно совместно.
LaTeX
$$$\\IsCompact(s) \\rightarrow \\ ContinuousOn (toFun{ s } f) s \\timesˢ {a \\mid 0 \\le a \\ \\\\land spectrum 𝕜 a ⊆ s} \\rightarrow \\ ContinuousOn (\\lambda fa: (𝕜 →ᵤ[{ s }] 𝕜) \\times A \\mapsto cfc (toFun{ s } fa.1) fa.2) fa$$$
Lean4
/-- Let `s : Set ℝ≥0` be a compact set and consider pairs `(f, a) : (ℝ≥0 → ℝ≥0) × A` where `f` is
continuous on `s` and `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} ×ˢ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}) :=
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1 (fun f hf ↦ continuousOn_cfc_nnreal A hs ((toFun { s }) f) hf)
(fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfc_fun_of_subset a ha')
