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 < 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) :
iFinset.filter (fun (x : ) => j < c ^ x) (Finset.range N), 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) :
iFinset.filter (fun (x : ) => j < c ^ x⌋₊) (Finset.range N), 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.