Proofs of the asymptotic forms of the density theorems

This module proves the asymptotic density theorems, deriving them from the explicit threshold forms Combinatorics.Line.exists_of_density and Combinatorics.ArithmeticProgression.exists_of_density_nat developed in this repository.

A combinatorial line in the cube of words of length n over a finite alphabet α is a family of #α words, one for each letter x : α, obtained from a single pattern by filling every occurrence of a wildcard with x; at least one coordinate must be a wildcard, so distinct letters give distinct words. This is Mathlib's Combinatorics.Line α (Fin n), and l x is the word of the line indexed by the letter x.

theorem Combinatorics.Line.exists_of_density_atTop (α : Type u_1) [Fintype α] (δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (Fin n → α)), δ * ↑(Fintype.card α) ^ n ≤ ↑A.card → ∃ (l : Line α (Fin n)), ∀ (x : α), ↑l x ∈ A

The Density Hales--Jewett theorem: for a positive density δ, every sufficiently long word length n has the property that any set of at least a δ fraction of the words of length n over α contains a combinatorial line.

theorem Combinatorics.ArithmeticProgression.exists_of_density_nat_atTop (k : ℕ) (hk : 3 ≤ k) (δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ A ⊆ Finset.range n, δ * ↑n ≤ ↑A.card → ∃ (a : ℕ) (d : ℕ), d ≠ 0 ∧ ∀ (i : Fin k), a + ↑i * d ∈ A

Szemeredi's theorem: for a positive density δ, every sufficiently large n has the property that any subset of range n of size at least δ * n contains an arithmetic progression of length k, i.e. k terms a, a + d, a + 2 * d, … with d ≠ 0.