English
Joint continuity of cfc on a product set of functions and spectral predicates, under compactness of s.
Русский
Совместная непрерывность cfc на произведении множества функций и спектральных условий, при компактности s.
LaTeX
$$$\\text{continuousOn_prod_of_continuousOn_lipschitzOnWith} \\_ \\rightarrow 1 \\rightarrow \\text{(условия на } f\\text{ и } a) \\Rightarrow \\text{continuousOn}$$$
Lean4
/-- The function `f ↦ cfcₙ f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{quasispectrum R a}] R`) on those functions which are continuous on
the quasispectrum and map zero to itself. -/
theorem lipschitzOnWith_cfcₙ_fun (a : A) :
LipschitzOnWith 1 (fun f ↦ cfcₙ (toFun {quasispectrum R a} f) a)
{f | ContinuousOn (toFun {quasispectrum R a} f) (quasispectrum R a) ∧ f 0 = 0} :=
by
by_cases ha : p a
· rintro f ⟨hf, hf0⟩ g ⟨hg, hg0⟩
simp only
rw [cfcₙ_apply .., cfcₙ_apply .., isometry_cfcₙHom (R := R) a ha |>.edist_eq]
simp only [ENNReal.coe_one, one_mul]
rw [← ContinuousMapZero.isometry_toContinuousMap.edist_eq, edist_continuousRestrict_of_singleton hf hg]
· simpa [cfcₙ_apply_of_not_predicate a ha] using LipschitzWith.const' 0 |>.lipschitzOnWith
