Theorems · Theorem · number theory

roth_3ap_theorem

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Fintype G] (ε : ℝ),
  0 < ε → cornersTheoremBound ε ≤ Fintype.card G → ∀ (A : Finset G), ε * ↑(Fintype.card G) ≤ ↑A.card → ¬ThreeAPFree ↑A

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.

Defined in

Mathlib.Combinatorics.Additive.Corner.Roth

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupFintype