Documentation

Mathlib.Analysis.SpecificLimits.FloorPow

Results on discretized exponentials #

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

theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (u : ) (l : ) (hmono : Monotone u) (hlim : ∀ (a : ), 1 < ac, (∀ᶠ (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.