Erdős Problem 264

Reference: erdosproblems.com/264

def Erdos264.IsIrrationalitySequence (a : ℕ → ℕ) : Prop

A sequence $a_n$ of integers is called an irrationality sequence if for every bounded sequence of integers $b_n$ with $a_n + b_n \neq 0$ and $b_n \neq 0$ for all $n$, the sum $$ \sum \frac{1}{a_n + b_n} $$ is irrational. Note: there are other possible definitions of this concept.

Equations

• Erdos264.IsIrrationalitySequence a = ∀ (b : ℕ → ℕ), BddAbove (Set.range b) → 0 ∉ Set.range (a + b) → 0 ∉ Set.range b → Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑(b n)))

theorem Erdos264.erdos_264.parts.i : ¬IsIrrationalitySequence fun (x : ℕ) => 2 ^ x

Is $2^n$ an example of an irrationality sequence? Kovač and Tao proved that it is not [KoTa24]

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

theorem Erdos264.erdos_264.parts.ii : IsIrrationalitySequence Nat.factorial ↔ sorry

Is $n!$ an example of an irrationality sequence?

theorem Erdos264.erdos_264.variants.example : IsIrrationalitySequence fun (n : ℕ) => 2 ^ 2 ^ n

One example is $2^{2^n}$.

theorem Erdos264.erdos_264.variants.ko_tao_neg {a : ℕ → ℕ} (h₁ : StrictMono a) (h₂ : 0 ∉ Set.range a) (h₃ : Summable fun (x : ℕ) => 1 / ↑(a x)) (h₄ : 0 < Filter.liminf (fun (n : ℕ) => ↑(a n) ^ 2 * ∑' (k : ↑(Set.Ioi n)), 1 / ↑(a ↑k) ^ 2) Filter.atTop) : ¬IsIrrationalitySequence a

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers $a_n$ such that $\sum\frac{1}{a_n}$ converges and $$ \liminf(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).

theorem Erdos264.erdos_264.variants.ko_tao_pos {F : ℕ → ℕ} (hF : Filter.Tendsto (fun (n : ℕ) => ↑(F (n + 1)) / ↑(F n)) Filter.atTop Filter.atTop) : ∃ (a : ℕ → ℕ), IsIrrationalitySequence a ∧ Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(a n)) fun (n : ℕ) => ↑(F n)

On the other hand, Kovač and Tao [KoTa24] do prove that for any function $F$ with $\lim F(n + 1) / F(n) = \infty$ there exists such an irrationality sequence with $a_n\sim F(n)$.

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