Erdős Problem 1051

Reference: erdosproblems.com/1051

def Erdos1051.GrowthCondition (a : ℕ → ℤ) : Prop

A sequence of integers a satisfies the growth condition if $\liminf a_n^{\frac{1}{2^n}} > 1$.

Equations

• Erdos1051.GrowthCondition a = (Filter.liminf (fun (n : ℕ) => ↑(a n) ^ (1 / 2 ^ n)) Filter.atTop > 1)

noncomputable def Erdos1051.ErdosSeries (a : ℕ → ℤ) : ℝ

The series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$.

Equations

• Erdos1051.ErdosSeries a = ∑' (n : ℕ), 1 / (↑(a n) * ↑(a (n + 1)))

theorem Erdos1051.erdos_1051 : (∀ (a : ℕ → ℤ), StrictMono a → GrowthCondition a → Irrational (ErdosSeries a)) ↔ sorry

Is it true that if $a_0 < a_1 < a_2 < \cdots$ is a strictly increasing sequence of integers with $\liminf a_n^{1/2^n} > 1$, then the series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$ is irrational?

theorem Erdos1051.erdos_1051.rapid_growth (a : ℕ → ℤ) (h_mono : StrictMono a) (h_rapid : ∃ C > 0, ∀ (n : ℕ), ↑(a (n + 1)) ≥ C * ↑(a n) ^ 2) : Irrational (ErdosSeries a)

Erdős [Er88c] notes that if the sequence grows rapidly to infinity (specifically, if $a_{n+1} \geq C \cdot a_n^2$ for some constant $C > 0$), then the series is irrational.

[Er88c] Erdős, P., On the irrationality of certain series: problems and results. New advances in transcendence theory (Durham, 1986) (1988), 102-109.