Theorems · Theorem · sequences and series

TFAE_exists_lt_isLittleO_pow

∀ (f : ℕ → ℝ) (R : ℝ),
  [∃ a ∈ Set.Ioo (-R) R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[Filter.atTop] fun x => a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[Filter.atTop] fun x => a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n].TFAE

Various statements equivalent to the fact that f n grows exponentially slower than R ^ n. * 0: $f n = o(a ^ n)$ for some $-R < a < R$; * 1: $f n = o(a ^ n)$ for some $0 < a < R$; * 2: $f n = O(a ^ n)$ for some $-R < a < R$; * 3: $f n = O(a ^ n)$ for some $0 < a < R$; * 4: there exist a < R and C such that one of C and R is positive and $|f n| ≤ Ca^n$ for all n; * 5: there exists 0 < a < R and a positive C such that $|f n| ≤ Ca^n$ for all n; * 6: there exists a < R such that $|f n| ≤ a ^ n$ for sufficiently large n; * 7: there exists 0 < a < R such that $|f n| ≤ a ^ n$ for sufficiently large n. NB: For backwards compatibility, if you add more items to the list, please append them at the end of the list.

Defined in

Mathlib.Analysis.SpecificLimits.Normed

Cited by

4 results in Mathlib

Foundations

Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound