English
Same as tendsto_cfcₙ_fun above: uniform convergence on quasispectrum implies convergence of cfcₙ.
Русский
То же, что и выше: равномерная схождения на квази-спектре приводит к сходимости cfcₙ.
LaTeX
$$$\\text{TendstoUniformlyOn } F f l (\\text{quasispectrum } R a) \\rightarrow \\text{Eventual}(x, ContinuousOn (F x) (\\text{quasispectrum } R a)) \\rightarrow \\ Tendsto (x \\mapsto cfcₙ (F x) a) l (nhds (cfcₙ f a))$$$
Lean4
/-- If `F : X → R → R` tends to `f : R → R` uniformly on the spectrum of `a`, and all
these functions are continuous on the spectrum and map zero to itself, then
`fun x ↦ cfcₙ (F x) a` tends to `cfcₙ f a`. -/
theorem tendsto_cfcₙ_fun {l : Filter X} {F : X → R → R} {f : R → R} {a : A}
(h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)) (hF : ∀ᶠ x in l, ContinuousOn (F x) (quasispectrum R a))
(hF0 : ∀ᶠ x in l, F x 0 = 0) : Tendsto (fun x ↦ cfcₙ (F x) a) l (𝓝 (cfcₙ f a)) := by
open scoped
NonUnitalContinuousFunctionalCalculus in
obtain (rfl | hl) := l.eq_or_neBot
· simp
have hf := h_tendsto.continuousOn hF
have hf0 : f 0 = 0 :=
Eq.symm <|
tendsto_nhds_unique (tendsto_const_nhds.congr' <| .symm hF0) <|
h_tendsto.tendsto_at (quasispectrum.zero_mem R a)
by_cases ha : p a
· let s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
have hs : s ∈ l := hF.and hF0
rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
conv =>
enter [1, x]
rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]
rw [cfcₙ_apply ..]
apply cfcₙHom_continuous _ |>.tendsto _ |>.comp
rw [ContinuousMapZero.isEmbedding_toContinuousMap.isInducing.tendsto_nhds_iff]
change Tendsto (fun x : s ↦ (⟨_, x.2.1.restrict⟩ : C(quasispectrum R a, R))) _ (𝓝 ⟨_, hf.restrict⟩)
rw [hf.tendsto_restrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
intro t
simp only [eventually_comap, Subtype.forall]
peel h_tendsto t with ht x _
simp_all
· simpa [cfcₙ_apply_of_not_predicate a ha] using tendsto_const_nhds
