Theorems · Theorem · sequences and series

tendsto_div_of_monotone_of_tendsto_div_floor_pow

∀ (u : ℕ → ℝ) (l : ℝ),
  Monotone u →
    ∀ (c : ℕ → ℝ),
      (∀ (k : ℕ), 1 < c k) →
        Filter.Tendsto c Filter.atTop (nhds 1) →
          (∀ (k : ℕ), Filter.Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) Filter.atTop (nhds l)) →
            Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (nhds l)

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 cs converging to 1.

Defined in

Mathlib.Analysis.SpecificLimits.FloorPow

Cited by

1 results in Mathlib

Foundations

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