English
As above, the cfc application is continuous under uniform convergence on spectrum.
Русский
Как выше, применение cfc имеет свойство непрерывности при равномерной сходимости на спектре.
LaTeX
$$$\\text{TendstoUniformlyOn } F f l (spectrum R a) \\land (\\forall x, ContinuousOn(Fx, spectrum R a)) \\Rightarrow \\ Tendsto (x \\mapsto cfc (F x) a) l (nhds (cfc f a))$$$
Lean4
/-- The function `f ↦ cfc f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{spectrum R a}] R`) on those functions which are continuous on
the spectrum. -/
theorem lipschitzOnWith_cfc_fun (a : A) :
LipschitzOnWith 1 (fun f ↦ cfc (toFun {spectrum R a} f) a)
{f | ContinuousOn (toFun {spectrum R a} f) (spectrum R a)} :=
by
by_cases ha : p a
· intro f hf g hg
simp only
rw [cfc_apply .., cfc_apply .., isometry_cfcHom (R := R) a ha |>.edist_eq]
simp only [ENNReal.coe_one, one_mul]
rw [edist_continuousRestrict_of_singleton hf hg]
· simpa [cfc_apply_of_not_predicate a ha] using LipschitzWith.const' 0 |>.lipschitzOnWith
