The corners theorem and Roth's theorem #

This file proves the corners theorem and Roth's theorem on arithmetic progressions of length three.

References #

[Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]
Wikipedia, Corners theorem

noncomputable def cornersTheoremBound (ε : ℝ) :

An explicit form for the constant in the corners theorem.

Note that this depends on SzemerediRegularity.bound, which is a tower-type exponential. This means cornersTheoremBound is in practice absolutely tiny.

Equations

Instances For

theorem corners_theorem {G : Type u_1} [AddCommGroup G] [Fintype G] (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ Fintype.card G) (A : Finset (G × G)) (hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card) :

The corners theorem for finite abelian groups.

The maximum density of a corner-free set in G × G goes to zero as |G| tends to infinity.

theorem corners_theorem_nat {n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n) (A : Finset (ℕ × ℕ)) (hAn : A ⊆ Finset.range n ×ˢ Finset.range n) (hAε : ε * ↑n ^ 2 ≤ ↑A.card) :

The corners theorem for ℕ.

The maximum density of a corner-free set in {1, ..., n} × {1, ..., n} goes to zero as n tends to infinity.

theorem roth_3ap_theorem {G : Type u_1} [AddCommGroup G] [Fintype G] (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ Fintype.card G) (A : Finset G) (hAε : ε * ↑(Fintype.card G) ≤ ↑A.card) :

Roth's theorem for finite abelian groups.

The maximum density of a 3AP-free set in G goes to zero as |G| tends to infinity.

theorem roth_3ap_theorem_nat {n : ℕ} (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound (ε / 3) ≤ n) (A : Finset ℕ) (hAn : A ⊆ Finset.range n) (hAε : ε * ↑n ≤ ↑A.card) :

Roth's theorem for ℕ.

The maximum density of a 3AP-free set in {1, ..., n} goes to zero as n tends to infinity.

(fun (N : ℕ) => ↑(rothNumberNat N)) =o[Filter.atTop] fun (N : ℕ) => ↑N

Roth's theorem for ℕ as an asymptotic statement.

The maximum density of a 3AP-free set in {1, ..., n} goes to zero as n tends to infinity.