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 : Nat → Real) (l : Real) (hmono : Monotone u) (hlim : ∀ (a : Real), LT.lt 1 a → Exists fun (c : Nat → Nat) => And (Filter.Eventually (fun (n : Nat) => LE.le (c (HAdd.hAdd n 1)).cast (HMul.hMul a (c n).cast)) Filter.atTop) (And (Filter.Tendsto c Filter.atTop Filter.atTop) (Filter.Tendsto (fun (n : Nat) => HDiv.hDiv (u (c n)) (c n).cast) Filter.atTop (nhds l)))) : Filter.Tendsto (fun (n : Nat) => HDiv.hDiv (u n) n.cast) 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 : Nat → Real) (l : Real) (hmono : Monotone u) (c : Nat → Real) (cone : ∀ (k : Nat), LT.lt 1 (c k)) (clim : Filter.Tendsto c Filter.atTop (nhds 1)) (hc : ∀ (k : Nat), Filter.Tendsto (fun (n : Nat) => HDiv.hDiv (u (Nat.floor (HPow.hPow (c k) n))) (Nat.floor (HPow.hPow (c k) n)).cast) Filter.atTop (nhds l)) : Filter.Tendsto (fun (n : Nat) => HDiv.hDiv (u n) n.cast) 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 : Nat) {j : Real} (hj : LT.lt 0 j) {c : Real} (hc : LT.lt 1 c) : LE.le ((Finset.filter (fun (i : Nat) => LT.lt j (HPow.hPow c i)) (Finset.range N)).sum fun (i : Nat) => HDiv.hDiv 1 (HPow.hPow (HPow.hPow c i) 2)) (HDiv.hDiv (HMul.hMul (HPow.hPow c 3) (Inv.inv (HSub.hSub c 1))) (HPow.hPow 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 : Real} (hc : LT.lt 1 c) (i : Nat) : LE.le (HMul.hMul (HSub.hSub 1 (Inv.inv c)) (HPow.hPow c i)) (Nat.floor (HPow.hPow c i)).cast

theorem sum_div_nat_floor_pow_sq_le_div_sq (N : Nat) {j : Real} (hj : LT.lt 0 j) {c : Real} (hc : LT.lt 1 c) : LE.le ((Finset.filter (fun (i : Nat) => LT.lt j (Nat.floor (HPow.hPow c i)).cast) (Finset.range N)).sum fun (i : Nat) => HDiv.hDiv 1 (HPow.hPow (Nat.floor (HPow.hPow c i)).cast 2)) (HDiv.hDiv (HMul.hMul (HPow.hPow c 5) (HPow.hPow (Inv.inv (HSub.hSub c 1)) 3)) (HPow.hPow j 2))

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