English
Roth’s theorem for finite abelian groups: in G, the maximum density of a 3-term-AP-free subset tends to zero as |G| grows; equivalently, for ε>0 and large G with density constraints, a subset of G has a 3-term progression.
Русский
Теорема Рота для конечных абелевых групп: максимальная плотность множества без трехчленников арифметических прогрессий в G стремится к нулю по мере роста |G|; следовательно, при заданной плотности такое множество не может быть трипорядочной прогрессией свободным.
LaTeX
$$$\forall \varepsilon>0,\ h_G: cornersTheoremBound(\varepsilon) \le |G|,\ A \subseteq G,\ h_{A\varepsilon}: \varepsilon \cdot |G| \le |A| \Rightarrow \neg ThreeAPFree(A).$$$
Lean4
/-- **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 (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ card G) (A : Finset G)
(hAε : ε * card G ≤ #A) : ¬ThreeAPFree (A : Set G) :=
by
rintro hA
classical
let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
have : ε * card G ^ 2 ≤ #B :=
by
calc
_ = card G * (ε * card G) := by ring
_ ≤ card G * #A := by gcongr
_ = #B := ?_
norm_cast
rw [← card_univ, ← card_product]
exact card_equiv ((Equiv.refl _).prodShear fun a ↦ Equiv.addLeft a) (by simp [B])
obtain ⟨x₁, y₁, x₂, y₂, hx₁y₁, hx₁y₂, hx₂y₁, hxy, hx₁x₂⟩ :
∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂ := by
simpa [IsCornerFree, isCorner_iff, B, -exists_and_left, -exists_and_right] using corners_theorem ε hε hG B this
have :=
hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
rw [sub_add_sub_comm, add_comm, add_sub_add_comm, add_right_cancel_iff, sub_eq_sub_iff_add_eq_add, add_comm, hxy,
add_comm]
exact hx₁x₂ <| by simpa using this.symm
