Erdős Problem 817

Reference: erdosproblems.com/817

noncomputable def Erdos817.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

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

theorem Erdos817.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 Erdos817.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)}}. $$