Erdős Problem 267

Reference: erdosproblems.com/267

theorem erdos_267 : (∀ (n : ℕ → ℕ), ∀ c > 1, StrictMono n → (∀ (k : ℕ), c ≤ ↑(n (k + 1)) / ↑(n k)) → Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))) ↔ sorry

Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n−1}$ be the Fibonacci sequence. Let $n_1 < n_2 < ...$ be an infinite sequence with $\frac{n_{k+1}}{n_k} ≥ c > 1$. Must $\sum_k \frac 1 {F_{n_k}}$ be irrational?

theorem erdos_267.variants.generalisation_ratio_limit_to_infinity : (∀ (n : ℕ → ℕ), StrictMono n → Filter.Tendsto (fun (k : ℕ) => ↑(n (k + 1)) / ↑k.succ) Filter.atTop Filter.atTop → Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))) ↔ sorry

Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n−1}$ be the Fibonacci sequence. Let $n_1 < n_2 < ...$ be an infinite sequence with $\frac {n_k}{k} → ∞$. Must $\sum_k \frac 1 {F_{n_k}}$ be irrational?

theorem erdos_267.variants.specialization_pow_two : Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (2 ^ k)))

Good [Go74] and Bicknell and Hoggatt [BiHo76] have shown that $\sum_n \frac 1 {F_{2^n}}$ is irrational.

Ref:

• [Go74] Good, I. J., A reciprocal series of Fibonacci numbers
• [BiHo76] Hoggatt, Jr., V. E. and Bicknell, Marjorie, A reciprocal series of Fibonacci numbers with subscripts $2\sp{n}k$

theorem erdos_267.variants.fibonacci_inverse_sum : Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib k))

The sum $\sum_n \frac 1 {F_{n}}$ itself was proved to be irrational by André-Jeannin.

Ref: André-Jeannin, Richard, Irrationalité de la somme des inverses de certaines suites récurrentes.