Erdős Problem 817

Reference: erdosproblems.com/817

def IsFiniteAPWith (k d : ℕ) (s : Set ℕ) : Prop

A finite arithmetic progression of length $k$ and difference $d$ is a set of the form $\{a_0, a_0 + d, a_0 + 2d, ..., a_0 + (k - 1) d\}$.

Equations

• IsFiniteAPWith k d s = ∃ (a₀ : ℕ), s = {x : ℕ | ∃ (i : Fin k), a₀ + ↑i * d = x}

theorem IsFiniteAP.zero {d : ℕ} {s : Set ℕ} : IsFiniteAPWith 0 d s ↔ s = ∅

Only the empty set is a finite arithmetic progression of length $0$.

theorem IsFiniteAP.one {d : ℕ} {s : Set ℕ} : IsFiniteAPWith 1 d s ↔ ∃ (a₀ : ℕ), s = {a₀}

Only singletons are finite arithmetic progressions of length $1$.

theorem IsFiniteAP.zero_diff {k : ℕ} [NeZero k] {s : Set ℕ} : IsFiniteAPWith k 0 s ↔ ∃ (a₀ : ℕ), s = {a₀}

Only singletons are finite arithmetic progressions of difference $0$.

def ContainsNontrivialAP (k : ℕ) (s : Set ℕ) : Prop

A set $s$ contains a non-trivial $k$-term, if there is a difference $d$ such that $s$ is a $k$-term progression with that difference and it contains more than 1 element.

Equations

• ContainsNontrivialAP k s = ∃ (d : ℕ), IsFiniteAPWith k d s ∧ 1 < s.ncard

noncomputable def g (k n : ℕ) : ℕ

Define $g_k(n)$ to be the minimal $N$ such that $\{1, ..., N\}$ contains some $A$ of size $|A| = n$ such that $$ \langle A\rangle = \left\{\sum_{a \in A} \epsilon_a a : \epsilon_a \in\{0, 1\}\right\} $$ contains no non-trivial $k$-term arithmetic progression.

Equations

• g k n = sInf {N : ℕ | ∃ A ⊆ Finset.Icc 1 N, A.card = n ∧ ∀ s ⊆ {x : ℕ | ∃ B ∈ A.powerset, ∑ a ∈ B, a = x}, ¬ContainsNontrivialAP k s}

theorem erdos_817 : ((fun (n : ℕ) => 3 ^ n) =O[Filter.atTop] fun (n : ℕ) => ↑(g 3 n)) ↔ sorry

Let $k\geq 3$. Define $g_k(n)$ to be the minimal $N$ such that $\{1, ..., N\}$ contains some $A$ of size $|A| = n$ such that $$ \langle A\rangle = \left\{\sum_{a \in A} \epsilon_a a : \epsilon_a \in\{0, 1\}\right\} $$ contains no non-trivial $k$-term arithmetic progression. Estimate $g_k(n)$. In particular, is it true that $$ g_3(n) \gg 3^n $$

theorem erdos_817.variants.bdd_power : ∃ O > 0, (fun (n : ℕ) => 3 ^ n / ↑n ^ O) =O[Filter.atTop] fun (n : ℕ) => ↑(g 3 n)

A problem of Erdős and Sárközy who proved $$ g_3(n) \gg \frac{3^n}{n^{O(1)}}. $$