English
If a sequence of continuous linear maps converges pointwise to g and is Cauchy in operator norm, then it converges to g in norm.
Русский
Если последовательность непрерывных линейных отображений сходится по точкам к g и является фундаментальной как операторы по норме, то она сходится к g по норме.
LaTeX
$$$\\text{Tendsto } (n\\mapsto f_n)\\;\\text{atTop} \\; (\\nhds\, g) \\,\\land\\, \\text{CauchySeq } f \\Rightarrow \\text{Tendsto } f\\;\\text{atTop} \\; (\\nhds\, g)$$$
Lean4
/-- If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise,
then it converges to the same map in norm. This lemma is used to prove that the space of continuous
linear maps is complete provided that the codomain is a complete space. -/
theorem tendsto_of_tendsto_pointwise_of_cauchySeq {f : ℕ → E' →SL[σ₁₂] F} {g : E' →SL[σ₁₂] F}
(hg : Tendsto (fun n x => f n x) atTop (𝓝 g)) (hf : CauchySeq f) : Tendsto f atTop (𝓝 g) := by
/- Since `f` is a Cauchy sequence, there exists `b → 0` such that `‖f n - f m‖ ≤ b N` for any
`m, n ≥ N`. -/
rcases cauchySeq_iff_le_tendsto_0.1 hf with
⟨b, hb₀, hfb, hb_lim⟩
-- Since `b → 0`, it suffices to show that `‖f n x - g x‖ ≤ b n * ‖x‖` for all `n` and `x`.
suffices ∀ n x, ‖f n x - g x‖ ≤ b n * ‖x‖ from
tendsto_iff_norm_sub_tendsto_zero.2
(squeeze_zero (fun n => norm_nonneg _) (fun n => opNorm_le_bound _ (hb₀ n) (this n)) hb_lim)
intro n x
have : Tendsto (fun m => ‖f n x - f m x‖) atTop (𝓝 ‖f n x - g x‖) :=
(tendsto_const_nhds.sub <| tendsto_pi_nhds.1 hg _).norm
refine
le_of_tendsto this
(eventually_atTop.2 ⟨n, fun m hm => ?_⟩)
-- This inequality follows from `‖f n - f m‖ ≤ b n`.
exact (f n - f m).le_of_opNorm_le (hfb _ _ _ le_rfl hm) _
