English
If a sequence is scaled by a factor c_n in a nontrivially normed field, and the scaled sequence c_n d_n converges to some y, while ‖c_n‖ tends to infinity along the index, then the original sequence d_n converges to 0.
Русский
Если последовательность d_n в нормированном пространстве приводится в соответствие к некоторому y после домножения на скаляр c_n, причём ‖c_n‖ стремится к бесконечности, и c_n d_n → y, то d_n → 0.
LaTeX
$$$\\forall \\alpha\\, (l : \\text{Filter } \\alpha)\\, (c : \\alpha \\to \\mathbb{K})\\, (d : \\alpha \\to E)\\, (y : E), \n\\left( \\ Tendsto (\\lambda n. \\|c(n)\\|) \\, l \\, \\text{atTop} \\Rightarrow \n Tendsto (\\lambda n. c(n) \\cdot d(n)) \\, l \\, (\\mathcal{N}(y)) \\right) \\, \\Longrightarrow \n Tendsto d \\, l \\, (\\mathcal{N}(0))$$$
Lean4
/-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
the sequence `d` tends to 0 at infinity. -/
theorem lim_zero {α : Type*} (l : Filter α) {c : α → 𝕜} {d : α → E} (hc : Tendsto (fun n => ‖c n‖) l atTop)
(hd : Tendsto (fun n => c n • d n) l (𝓝 y)) : Tendsto d l (𝓝 0) :=
by
have : ∀ᶠ n in l, (c n)⁻¹ • c n • d n = d n :=
(eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn ↦ inv_smul_smul₀ hn (d n)
rw [tendsto_norm_atTop_iff_cobounded] at hc
simpa using Tendsto.congr' this <| (tendsto_inv₀_cobounded.comp hc).smul hd
