English
In a finite abelian group G, the maximum density of a corner-free subset of G × G tends to zero as |G| grows. More precisely, if A ⊆ G × G has density at least ε and |G| is large enough (at least cornersTheoremBound ε), then A is not corner-free.
Русский
Для конечной абелевой группы G максимальная плотность множества без угла в G × G стремится к нулю при бесконечном росте |G|. Если A ⊆ G × G имеет плотность не меньше ε и |G| достаточно велик (не меньше cornersTheoremBound ε), то A содержит угол.
LaTeX
$$$\forall \varepsilon>0,\ h_\varepsilon: 0<\varepsilon,\ h_G: cornersTheoremBound(\varepsilon) \le |G|,\ A \subseteq G \times G,\ h_{A\varepsilon}: \varepsilon \cdot |G|^2 \le |A| \Rightarrow \neg IsCornerFree(A).$$$
Lean4
/-- 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 (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ card G) (A : Finset (G × G))
(hAε : ε * card G ^ 2 ≤ #A) : ¬IsCornerFree (A : Set (G × G)) :=
by
rintro hA
rw [cornersTheoremBound, Nat.add_one_le_iff] at hG
have hε₁ : ε ≤ 1 := by
have := hAε.trans (Nat.cast_le.2 A.card_le_univ)
simp only [sq, Nat.cast_mul, Fintype.card_prod] at this
rwa [mul_le_iff_le_one_left] at this
positivity
have := noAccidental hA
rw [Nat.floor_lt' (by positivity), inv_lt_iff_one_lt_mul₀' (by positivity)] at hG
refine hG.not_ge (le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < card G ^ 2))
classical
have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
rw [card_triangles, card_triangleIndices] at h₁
convert h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1 <;> simp <;> ring
