Difference sets of full-dimensional lattice sets

DefinitionFull-dimensional sets in \(\mathbb{Z}^d\)#✓fully proved

A finite set \(A \subseteq \mathbb{Z}^d\) is full-dimensional when it is not contained in an affine hyperplane: for every real vector \(a \in \mathbb{R}^d\) and every real number \(c\), if \(\sum_i a_i x_i = c\) for all \(x \in A\), then \(a = 0\).

def IsFullDimensional {d : ℕ} (A : Finset (Fin d → ℤ)) : Prop :=
  ∀ (a : Fin d → ℝ) (c : ℝ), (∀ x ∈ A, ∑ i, a i * x i = c) → a = 0

Used by 1

Used byStatement of Stanchescu's difference set bound

DefinitionStatement of Stanchescu's difference set bound#✓fully proved

The proposition that for every integer \(d \ge 2\) there is a natural number \(N\) such that every full-dimensional finite set \(A \subseteq \mathbb{Z}^d\) (one not contained in an affine hyperplane) with \(|A| \ge N\) satisfies \(|A - A| \ge \left(2d - 2 + \frac{1}{d - 1}\right)|A| - (2d^2 - 4d + 3)\), where \(A - A = \{a - b : a, b \in A\}\) is the difference set of \(A\).

def stanchescuDifferenceBound : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∃ N : ℕ, ∀ A : Finset (Fin d → ℤ), IsFullDimensional A → N ≤ A.card →
    (2 * d - 2 + 1 / (d - 1 : ℝ)) * A.card - (2 * d ^ 2 - 4 * d + 3) ≤ ((A - A).card : ℝ)

Uses 1 · Used by 1

Statement usesFull-dimensional sets in \(\mathbb{Z}^d\)

Used byConlon–Lim theorem: Stanchescu's difference set bound holds

TheoremConlon–Lim theorem: Stanchescu's difference set bound holds#●ready to prove

For every integer \(d \ge 2\) there is a natural number \(N\) such that every finite set \(A \subseteq \mathbb{Z}^d\) with \(|A| \ge N\) that is not contained in an affine hyperplane (no nonzero real linear functional is constant on \(A\)) satisfies \(|A - A| \ge \left(2d - 2 + \frac{1}{d - 1}\right)|A| - (2d^2 - 4d + 3)\), where \(A - A = \{a - b : a, b \in A\}\) is the difference set of \(A\).

public theorem_wanted stanchescuDifferenceBound_holds : stanchescuDifferenceBound

Sources

• Problems presented at the workshop on recent trends in additive combinatorics, collected by E. Croot and V. F. Lev, AIM workshop problem list, Problem 2.6 (Y. Stanchescu), https://aimath.org/WWN/additivecomb/additivecomb.pdf; resolution: D. Conlon and J. Lim, Difference sets in ℝ^d, Israel J. Math. 267 (2025) 729-748, arXiv:2110.09053, abstract and main theorem, https://arxiv.org/abs/2110.09053.

Uses 1

Statement usesStatement of Stanchescu's difference set bound

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.