English
A comprehensive equivalence (TFAE) for statements that a function f grows strictly slower than a^n, or is O(a^n) for various a in different ranges, including 0<a<R and negative a.
Русский
Полная эквивалентность (TFAE) для утверждений о том, что f растёт медленнее, чем a^n, или является O(a^n) для различных a в диапазонах, включая 0<a<R и отрицательные a.
LaTeX
$$TFAE_exists_lt_isLittleO_pow f R$$
Lean4
/-- If a monotone sequence `u` is such that `u ⌊c^n⌋₊ / ⌊c^n⌋₊` converges to a limit `l` for all
`c > 1`, then `u n / n` tends to `l`. It is even enough to have the assumption for a sequence of
`c`s converging to `1`. -/
theorem tendsto_div_of_monotone_of_tendsto_div_floor_pow (u : ℕ → ℝ) (l : ℝ) (hmono : Monotone u) (c : ℕ → ℝ)
(cone : ∀ k, 1 < c k) (clim : Tendsto c atTop (𝓝 1))
(hc : ∀ k, Tendsto (fun n : ℕ => u ⌊c k ^ n⌋₊ / ⌊c k ^ n⌋₊) atTop (𝓝 l)) : Tendsto (fun n => u n / n) atTop (𝓝 l) :=
by
apply tendsto_div_of_monotone_of_exists_subseq_tendsto_div u l hmono
intro a ha
obtain ⟨k, hk⟩ : ∃ k, c k < a := ((tendsto_order.1 clim).2 a ha).exists
refine
⟨fun n => ⌊c k ^ n⌋₊, ?_, (tendsto_nat_floor_atTop (α := ℝ)).comp (tendsto_pow_atTop_atTop_of_one_lt (cone k)),
hc k⟩
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c k ^ n⌋₊ := by
intro n
refine zero_lt_one.trans_le ?_
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]
have A :
Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / (⌊c k ^ n⌋₊ / c k ^ n)) atTop
(𝓝 (1 * c k / 1)) :=
by
refine Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero
· refine tendsto_nat_floor_div_atTop.comp ?_
exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)
· refine tendsto_nat_floor_div_atTop.comp ?_
exact tendsto_pow_atTop_atTop_of_one_lt (cone k)
have B : Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / ⌊c k ^ n⌋₊) atTop (𝓝 (c k)) :=
by
simp only [one_mul, div_one] at A
convert A using 1
ext1 n
field_simp [(zero_lt_one.trans (cone k)).ne']
ring
filter_upwards [(tendsto_order.1 B).2 a hk] with n hn
exact (div_le_iff₀ (H n)).1 hn.le
