Arithmetic progressions in dense sets

Density versions: Szemerédi's and Roth's theorems and Roth-number bounds, Sárközy's theorem, cap sets, counts of three-term progressions, progressions in complements and in walks, arithmetic progression API, and polynomial triangle removal in vector spaces.

• Arithmetic progressions and progression-free sets
• Bounds for Roth numbers
• Furstenberg–Sárközy theorem
• Number of arithmetic progressions in dense sets
• Polynomial triangle removal in vector spaces
• Progression-free sets meeting every infinite progression
• Progressions with differences from a difference set
• Small values of cap set sizes and Roth numbers
• Squares in dense subsets of the grid
• Three-term progressions in unit-step walks
• Unions of progression-free sets

TheoremSzemerédi's theorem#✓fully proved

For every natural number \(k \ge 1\) and every real number \(\delta > 0\) there is a natural number \(N\) such that for every \(n \ge N\), every set \(A \subseteq \{0, 1, \dots, n - 1\}\) with \(\delta n \le |A|\) contains an arithmetic progression of length \(k\): there are natural numbers \(a\) and \(d > 0\) with \(a + i d \in A\) for all \(i < k\).

Proof: We derive the result from the density Hales–Jewett theorem by averaging coordinate-sum translates and mapping combinatorial lines to arithmetic progressions.

public theorem szemeredi :
    ∀ k : ℕ, 0 < k → ∀ δ : ℝ, 0 < δ → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ A : Finset ℕ, A ⊆ Finset.range n → δ * (n : ℝ) ≤ (A.card : ℝ) →
        ∃ a d : ℕ, 0 < d ∧ ∀ i : ℕ, i < k → a + i * d ∈ A

Sources

• E. Szemerédi, Acta Arith. 27 (1975); Lean states finitary density form equivalent to infinitary positive upper density k-AP existence.

Uses 1 · Used by 1

Proof usesDensity Hales–Jewett theorem

Used byFurstenberg multiple recurrence theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.