Erdős Problem 359

Reference: erdosproblems.com/359

def Erdos359.IsGoodFor (A : ℕ → ℕ) (n : ℕ) : Prop

The predicate that A is monotone, A 0 = n and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos359.erdos_359.parts.i (A : ℕ → ℕ) (hA : IsGoodFor A 1) : Filter.Tendsto (fun (k : ℕ) => ↑(A k) / ↑k) Filter.atTop Filter.atTop

Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that $a_1=1$ and $a_{i+1}$ is the least integer which is not a sum of consecutive earlier $a_j$s. Show that $a_k / k \to \infty$.

theorem Erdos359.erdos_359.parts.ii (A : ℕ → ℕ) (hA : IsGoodFor A 1) (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (k : ℕ) => ↑(A k) / ↑k ^ (1 + c)) Filter.atTop Filter.atTop

Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that $a_1=1$ and $a_{i+1}$ is the least integer which is not a sum of consecutive earlier $a_j$s. Show that $a_k / k ^ {1 + c} \to 0$ for any $c > 0$.

theorem Erdos359.erdos_359.variants.isGoodFor_1_low_values (A : ℕ → ℕ) (hA : IsGoodFor A 1) : A '' Set.Iic 7 = {1, 2, 4, 5, 8, 10, 14, 15}

Suppose monotone sequence $A$ satisfies the following: A 0 = 1 and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j. Then the first few terms of $A$ are $1,2,4,5,8,10,14,15,...$.

theorem Erdos359.erdos_359.variants.isGoodFor_1_asymptotic (A : ℕ → ℕ) (hA : IsGoodFor A 1) : Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => ↑(A k)) fun (k : ℕ) => ↑k * Real.log ↑k / Real.log (Real.log ↑k)

Suppose monotone sequence $A$ satisfies the following: A 0 = 1 and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j. Then it is conjectured that $$a_k ~ \frac{k \log k}{\log \log k}$$.