English
For a fixed a and subset s with spectrum(a) ⊆ s, the map f ↦ cfc(toFun{ s } f) a is 1-Lipschitz on the set of f continuous on s.
Русский
Для фиксированного a и подмножества s с spectrum a ⊆ s отображение f ↦ cfc(toFun{ s } f) a грузоподъёмно 1-Липшицево на множества функций, непрерывных на s.
LaTeX
$$$a\\in A,\\; \\; (s: Set R),\\; spectrum\\,R\\,a \\subseteq s \\Rightarrow \\ Lip\\ schnitzonWith 1 (\\lambda f. cfc(toFun{ s } f) a) {f | ContinuousOn (toFun { s } f) s}$$$
Lean4
/-- The function `f ↦ cfcₙ f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{s}] R`) on those functions which are continuous on a set `s` containing
the quasispectrum and map zero to itself. -/
theorem lipschitzOnWith_cfcₙ_fun_of_subset (a : A) {s : Set R} (hs : quasispectrum R a ⊆ s) :
LipschitzOnWith 1 (fun f ↦ cfcₙ (toFun { s } f) a) {f | ContinuousOn (toFun { s } f) (s) ∧ f 0 = 0} :=
by
have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {quasispectrum R a}) (𝔗 := { s }) (β := R) (by simpa)
have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun { s } f) (s) ∧ f 0 = 0})
simpa using lipschitzOnWith_cfcₙ_fun R a |>.comp h₃ (fun f ↦ .imp_left fun hf ↦ hf.mono hs)
