Erdős problem 266
Let be an infinite sequence of positive integers such that converges. There exists some integer such that is irrational.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/266.lean¬∀ (a : ℕ → ℕ), ((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun x => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t))SolvedStatement only, no proof