Theorems · Theorem · number theory

roth_3ap_theorem_nat

∀ {n : ℕ} (ε : ℝ), 0 < ε → cornersTheoremBound (ε / 3) ≤ n → ∀ A ⊆ Finset.range n, ε * ↑n ≤ ↑A.card → ¬ThreeAPFree ↑A

Roth's theorem for ℕ. The maximum density of a 3AP-free set in {1, ..., n} goes to zero as n tends to infinity.

Defined in

Mathlib.Combinatorics.Additive.Corner.Roth

Cited by

1 results in Mathlib

Foundations

Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound