Erdős Problem 272

Reference: erdosproblems.com/272

def Erdos272.IsArithInterSet (N : ℕ) (A : Finset (Finset ℕ)) : Prop

Let $N \in\mathbb{N}$. We say that $\{A_1, ..., A_t\}\subseteq \mathcal{P}(\{1, \dots, N\})$ is an arithmetic intersection set if $A_i \cap A_j$ is a non-empty arithmetic progression for each $i \neq j$.

Equations

• Erdos272.IsArithInterSet N A = (A ⊆ (Finset.Icc 1 N).powerset ∧ (↑A).Pairwise fun (S T : Finset ℕ) => ∃ l > 0, (↑(S ∩ T)).IsAPOfLength l)

noncomputable def Erdos272.maxArithInterCard (N : ℕ) : ℕ

For each $N > 0$, let $t$ be the largest size of an arithmetic intersection set.

Equations

• Erdos272.maxArithInterCard N = sSup {x : ℕ | ∃ (A : Finset (Finset ℕ)) (_ : Erdos272.IsArithInterSet N A), A.card = x}

theorem Erdos272.erdos_272 : Asymptotics.IsEquivalent Filter.atTop (fun (N : ℕ) => ↑(maxArithInterCard N)) sorry

Let $N\geq 1$. What is the largest $t$ such that there are $A_1,\ldots,A_t\subseteq \{1,\ldots,N\}$ with $A_i\cap A_j$ a non-empty arithmetic progression for all $i\neq j$?

theorem Erdos272.erdos_272.variants.isBigO_sq : (fun (N : ℕ) => ↑(maxArithInterCard N)) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ 2

Simonovits and Sós have shown that $t\ll N^2$.

theorem Erdos272.erdos_272.variants.szabo : (fun (N : ℕ) => ↑(maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ (5 / 3) * Real.log ↑N ^ 3

Szabo showed that the maximal $t$ is equal to $$ \frac{N^2}{2} + O(N^{5/3}\log^3N). $$

theorem Erdos272.erdos_272.variants.szabo_strong : (fun (N : ℕ) => ↑(maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun (N : ℕ) => ↑N

Szabo asks whether the maximal $t$ is given by $$ \frac{N^2}{2} + O(N) $$