Results on discretized exponentials

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.atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Filter.Tendsto c Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => u (c n) / ↑(c 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 n / n tends to a limit l along subsequences with exponential growth rate arbitrarily close to 1, then u n / n tends to l.

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.atTop (nhds 1)) (hc : ∀ (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.

theorem sum_div_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) : (Finset.sum (Finset.filter (fun (x : ℕ) => j < c ^ x) (Finset.range N)) fun (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.

theorem mul_pow_le_nat_floor_pow {c : ℝ} (hc : 1 < c) (i : ℕ) : (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

theorem sum_div_nat_floor_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) : (Finset.sum (Finset.filter (fun (x : ℕ) => j < ↑⌊c ^ x⌋₊) (Finset.range N)) fun (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.