Results on discretized exponentials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We state several auxiliary results pertaining to sequences of the form ⌊c^n⌋₊.

tendsto_div_of_monotone_of_tendsto_div_floor_pow: 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.
sum_div_nat_floor_pow_sq_le_div_sq: The sum of 1/⌊c^i⌋₊^2 above a threshold j is comparable to 1/j^2, up to a multiplicative constant.

theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (u : ℕ → ℝ) (l : ℝ) (hmono : monotone u) (hlim : ∀ (a : ℝ), 1 < a → (∃ (c : ℕ → ℕ), (∀ᶠ (n : ℕ) in filter.at_top , ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ filter.tendsto c filter.at_top filter.at_top ∧ filter.tendsto (λ (n : ℕ), u (c n) / ↑(c n)) filter.at_top (nhds l))) :

filter.tendsto (λ (n : ℕ), u n / ↑n) filter.at_top (nhds l)

If a monotone sequence u is such that u n / n tends to a limit l along subsequences with exponential growth rate arbitrarily close to 1, then u n / n tends to l.

source

theorem tendsto_div_of_monotone_of_tendsto_div_floor_pow (u : ℕ → ℝ) (l : ℝ) (hmono : monotone u) (c : ℕ → ℝ) (cone : ∀ (k : ℕ), 1 < c k) (clim : filter.tendsto c filter.at_top (nhds 1)) (hc : ∀ (k : ℕ), filter.tendsto (λ (n : ℕ), u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) filter.at_top (nhds l)) :

filter.tendsto (λ (n : ℕ), u n / ↑n) filter.at_top (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.

source

theorem sum_div_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) :

(finset.filter (λ (i : ℕ), j < c ^ i) (finset.range N)).sum (λ (i : ℕ), 1 / (c ^ i) ^ 2) ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

The sum of 1/(c^i)^2 above a threshold j is comparable to 1/j^2, up to a multiplicative constant.

source

theorem mul_pow_le_nat_floor_pow {c : ℝ} (hc : 1 < c) (i : ℕ) :

(1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

source

theorem sum_div_nat_floor_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) :

(finset.filter (λ (i : ℕ), j < ↑⌊c ^ i⌋₊) (finset.range N)).sum (λ (i : ℕ), 1 / ↑⌊c ^ i⌋₊ ^ 2) ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

The sum of 1/⌊c^i⌋₊^2 above a threshold j is comparable to 1/j^2, up to a multiplicative constant.