Theorems · Theorem · number theory

corners_theorem_nat

• 1000+ list: Corners theorem

∀ {n : ℕ} {ε : ℝ},
  0 < ε →
    cornersTheoremBound (ε / 9) ≤ n → ∀ A ⊆ Finset.range n ×ˢ Finset.range n, ε * ↑n ^ 2 ≤ ↑A.card → ¬IsCornerFree ↑A

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.

Defined in

Mathlib.Combinatorics.Additive.Corner.Roth

Cited by

0 results in Mathlib

Foundations

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