Skip to content

Erdős problem 264

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers ana_n such that ∑1an\sum \frac{1}{a_n} converges and lim inf⁡n→∞(an2∑k>n1ak2)>0 \liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0 is not an irrationality sequence.

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

264.lean

Retained formal statement4 of 5

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers ana_n such that ∑1an\sum \frac{1}{a_n} converges and lim inf⁡n→∞(an2∑k>n1ak2)>0 \liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0 is not an irrationality sequence.

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

FormalConjectures/ErdosProblems/264.leanErdos264.erdos_264.variants.ko_tao_neg6 linesExact file
∀ {a : ℕ → ℕ},  StrictMono a →    0 ∉ Set.range a →      (Summable fun x => 1 / ↑(a x)) →        0 < Filter.liminf (fun n => ↑(a n) ^ 2 * ∑' (k : ↑(Set.Ioi n)), 1 / ↑(a ↑k) ^ 2) Filter.atTop →          ¬Erdos264.IsIrrationalitySequence a
SolvedStatement only, no proofformal statement reference

Search problems.science

Find a Problem, Result, source, or page