mathlib3documentation

analysis.specific_limits.floor_pow

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 (λ (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.

theorem tendsto_div_of_monotone_of_tendsto_div_floor_pow (u : ) (l : ) (hmono : monotone u) (c : ) (cone : (k : ), 1 < c k) (clim : (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.

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.

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.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.