sum_div_nat_floor_pow_sq_le_div_sq
theorem sum_div_nat_floor_pow_sq_le_div_sq :
∀ (N : ℕ) {j : ℝ},
0 < j →
∀ {c : ℝ},
1 < c →
((Finset.filter (fun x => j < ↑⌊c ^ x⌋₊) (Finset.range N)).sum fun i => 1 / ↑⌊c ^ i⌋₊ ^ 2) ≤
c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
The theorem `sum_div_nat_floor_pow_sq_le_div_sq` states that for any natural number `N`, any real number `j` greater than zero, and any real number `c` greater than one, the sum of the reciprocals of the square of the greatest integer less than or equal to `c` raised to the power `i` (`1/⌊c^i⌋₊^2`), where `i` ranges over all natural numbers less than `N` for which `j` is less than `⌊c^i⌋₊`, is less than or equal to `c^5 * (c - 1)⁻¹ ^ 3 / j^2`. This essentially compares the aforementioned sum with the reciprocal of the square of `j`, scaled by a factor that depends on `c`.
More concisely: For any natural number N, real number j > 0, and real number c > 1, the sum of 1/(⌊c^i⌋^2) for i < N with j < ⌊c^i⌋ is less than or equal to (c^5 * (c-1)^-3)/j^2.
|
tendsto_div_of_monotone_of_exists_subseq_tendsto_div
theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div :
∀ (u : ℕ → ℝ) (l : ℝ),
Monotone u →
(∀ (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)
The theorem `tendsto_div_of_monotone_of_exists_subseq_tendsto_div` states that for any monotone sequence of real numbers `u` and any real number `l`, if for every real number `a` greater than 1, there exists a subsequence `c` such that the value of `c(n + 1)` is at most `a` times the value of `c(n)` for all sufficiently large `n`, and if the subsequence `c` tends to infinity and the sequence `u(c(n)) / c(n)` tends to `l`, then the sequence `u(n) / n` also tends to `l` as `n` goes to infinity. The theorem thus provides a condition under which the average rate of growth of a monotone sequence is determined by the average rate of growth of its subsequences.
More concisely: If a monotone sequence `u` has a subsequence `c` that tends to infinity and satisfies `c(n+1)/c(n)≤a` for some `a>1` and all sufficiently large `n`, and if the quotients `u(c(n))/c(n)` converge to a limit `l`, then the sequence `u(n)/n` converges to `l` as `n` goes to infinity.
|
sum_div_pow_sq_le_div_sq
theorem sum_div_pow_sq_le_div_sq :
∀ (N : ℕ) {j : ℝ},
0 < j →
∀ {c : ℝ},
1 < c →
((Finset.filter (fun x => j < c ^ x) (Finset.range N)).sum fun i => 1 / (c ^ i) ^ 2) ≤
c ^ 3 * (c - 1)⁻¹ / j ^ 2
This theorem asserts that for any natural number `N` and any positive real number `j` greater than zero, along with another real number `c` greater than one, the sum of the reciprocals of the squares of `c` raised to the power of `i` (where `i` is in the range of `N` and `c` to the power of `i` is greater than `j`) is always less than or equal to `(c^3)/(j^2)` times the reciprocal of `(c - 1)`. In other words, for sufficiently high indices `i`, the sum of the squared reciprocals of the `i`th power of a number `c` is approximately the square reciprocal of `j`, scaled by a function of `c`.
More concisely: For any natural number N and positive real numbers j and c with c > 1, the sum of the reciprocals of the squares of c raised to the power of i (where i is in the range of N and c to the power of i exceeds j), is bounded above by (c^3 / (j^2)) * (1 / (c-1)).
|
tendsto_div_of_monotone_of_tendsto_div_floor_pow
theorem tendsto_div_of_monotone_of_tendsto_div_floor_pow :
∀ (u : ℕ → ℝ) (l : ℝ),
Monotone u →
∀ (c : ℕ → ℝ),
(∀ (k : ℕ), 1 < c k) →
Filter.Tendsto c Filter.atTop (nhds 1) →
(∀ (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)
The given theorem states that given a monotone sequence `u` of real numbers, and a real number `l`, if for every sequence `c` of real numbers such that all elements of `c` are greater than 1 and `c` tends to 1 as the index approaches infinity, the sequence `u ⌊c^n⌋₊ / ⌊c^n⌋₊` also converges to the limit `l`, then the sequence `u n / n` also converges to the limit `l`. In other words, if the ratio of `u` values at the floor of exponentially increasing indices to those indices tends to a limit `l`, then the ratio of `u n` to `n` also tends to that limit `l`.
More concisely: If a monotonic sequence `u` of real numbers and a limit `l` satisfy the condition that for every sequence `c > 1` converging to 1 as the index approaches infinity, the quotient `(u ⌊c^n⌋₊ / ⌊c^n⌋₊)` converges to `l`, then `(un / n)` also converges to `l`.
|