Squares in dense subsets of the grid

DefinitionErdős Problem 658 (axis-parallel squares in dense subsets of the grid)#✓fully proved

The statement that for every real number \(\delta > 0\) there is a natural number \(N_0\) such that for every \(N \ge N_0\), every set \(A \subseteq \{1, \dots, N\}^2\) of pairs of natural numbers with \(|A| \ge \delta N^2\) contains the four vertices \((a, b)\), \((a + d, b)\), \((a, b + d)\) and \((a + d, b + d)\) of an axis-parallel square, for some natural numbers \(a\), \(b\) and \(d \ge 1\).

def denseGridContainsSquare : Prop :=
  ∀ δ > (0 : ℝ), ∀ᶠ N : ℕ in Filter.atTop, ∀ A : Finset (ℕ × ℕ),
    A ⊆ Finset.Icc 1 N ×ˢ Finset.Icc 1 N → δ * (N : ℝ) ^ 2 ≤ A.card →
      ∃ a b d : ℕ, 0 < d ∧ (a, b) ∈ A ∧ (a + d, b) ∈ A ∧ (a, b + d) ∈ A ∧ (a + d, b + d) ∈ A

Used by 1

Used byErdős Problem 658 is true

TheoremErdős Problem 658 is true#●ready to prove

For every real number \(\delta > 0\) there is a natural number \(N_0\) such that for every \(N \ge N_0\), every set \(A \subseteq \{1, \dots, N\}^2\) of pairs of natural numbers with \(|A| \ge \delta N^2\) contains the four vertices \((a, b)\), \((a + d, b)\), \((a, b + d)\) and \((a + d, b + d)\) of an axis-parallel square, for some natural numbers \(a\), \(b\) and \(d \ge 1\).

This follows from the density Hales–Jewett theorem of Furstenberg and Katznelson; Solymosi gave a quantitative proof.

public theorem_wanted denseGridContainsSquare_holds : denseGridContainsSquare

Sources

• T. F. Bloom, Erdős Problems, Problem #658, https://www.erdosproblems.com/658 (status PROVED (LEAN)); resolution: H. Furstenberg and Y. Katznelson, A density version of the Hales-Jewett theorem, J. Anal. Math. (1991), 64-119, erdosproblems.com/658: the qualitative statement follows from the density Hales-Jewett theorem; a quantitative proof was given by Solymosi (Combin. Probab. Comput. 2004), https://www.erdosproblems.com/658.

Uses 1

Statement usesErdős Problem 658 (axis-parallel squares in dense subsets of the grid)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.