Erdős Problem 346

References:

• erdosproblems.com/346
• [Gr64d] Graham, R. L., A property of Fibonacci numbers. Fibonacci Quart. (1964), 1-10.
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem Erdos346.erdos_346 : sorry ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ (B : Set ℕ), B.Infinite → ¬IsAddComplete (Set.range A \ B)) → Filter.Tendsto (fun (n : ℕ) => ↑(A (n + 1)) / ↑(A n)) Filter.atTop (nhds ((1 + √5) / 2))

Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?

def Erdos346.f (n : ℕ) : ℕ

We define a sequence f by the formula f n = n.fib - (- 1) ^ n.

Equations

• Erdos346.f n = if Even n then Nat.fib n - 1 else Nat.fib n + 1

theorem Erdos346.erdos_346.f_isLacunary : IsLacunary f

The sequence f is lacunary.

theorem Erdos346.erdos_346.f_isAddStronglyCompleteNatSeq : IsAddStronglyCompleteNatSeq f

The sequence f is strongly complete, and this is proved in [Gr64d].

theorem Erdos346.erdos_346.f_not_isAddComplete {B : Set ℕ} (hB : B.Infinite) : ¬IsAddComplete (Set.range f \ B)

The sequence f is not complete whenever infinitely many terms are removed from it, and this is proved in [Gr64d].

theorem Erdos346.erdos_346.gt_goldenRatio_not_IsAddComplete {A : ℕ → ℕ} (hA : ∀ (n : ℕ), (1 + √5) / 2 * ↑(A n) < ↑(A (n + 1))) {B : Set ℕ} (hB : B.Infinite) : ¬IsAddComplete (Set.range A \ B)

Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.

theorem Erdos346.erdos_346.example : ∃ (A : ℕ → ℕ), IsLacunary A ∧ IsAddStronglyCompleteNatSeq A ∧ (∀ (B : Set ℕ), B.Infinite → ¬IsAddComplete (Set.range A \ B)) ∧ Filter.liminf (fun (n : ℕ) => ↑(A (n + 1)) / 2) Filter.atTop = 1 ∧ Filter.limsup (fun (n : ℕ) => ↑(A (n + 1)) / ↑(A n)) Filter.atTop = ⊤

Erdős and Graham [ErGr80] also say that it is not hard to construct very irregular sequences satisfying the aforementioned properties.