English
If f1•g tends to t, f1 is cobounded, and f1−f2 is bounded, then f2•g tends to t.
Русский
Если f1(x)•g(x) → t, f1(x) → cobounded и f1(x) − f2(x) ограничено, то f2(x)•g(x) → t.
LaTeX
$$$\text{Tendsto}(f_1\cdot g) \to t \land f_1 \to_{l} \text{cobounded}(K) \land \|f_1-f_2\| embarr ≤ C \Rightarrow \text{Tendsto}(f_2\cdot g) \to t$$$
Lean4
theorem eventually_div_lt_of_div_lt {L : ℝ} {n : ℕ} (hn : n ≠ 0) (hL : u n / n < L) : ∀ᶠ p in atTop, u p / p < L := by
/- It suffices to prove the statement for each arithmetic progression `(n * · + r)`. -/
refine
.atTop_of_arithmetic hn fun r _ =>
?_
/- `(k * u n + u r) / (k * n + r)` tends to `u n / n < L`, hence
`(k * u n + u r) / (k * n + r) < L` for sufficiently large `k`. -/
have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
(tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
(tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <|
by simpa
have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) :=
by
rw [add_zero, add_zero] at A
refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
simp only [add_div' _ _ _ hx, div_div_div_cancel_right₀ hx, mul_comm]
refine
((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk =>
?_
/- Finally, we use an upper estimate on `u (k * n + r)` to get an estimate on
`u (k * n + r) / (k * n + r)`. -/
rw [mul_comm]
refine lt_of_le_of_lt ?_ hk
simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
gcongr
apply h.apply_mul_add_le
