Sumsets of sets of density zero

DefinitionErdős Problem 245 on sumsets of sets of density zero#✓fully proved

For \(N \in \mathbb{N}\) write \([1, N] = \{1, \dots, N\}\), and for \(A \subseteq \mathbb{N}\) write \(A + A = \{a + b \mid a, b \in A\}\). This is the statement that for every infinite set \(A \subseteq \mathbb{N}\) with \(\lvert A \cap [1, N] \rvert / N \to 0\) as \(N \to \infty\) and every real \(\varepsilon > 0\), there are infinitely many \(N\) with \(\lvert (A + A) \cap [1, N] \rvert > (3 - \varepsilon) \lvert A \cap [1, N] \rvert\). This expresses \(\limsup_{N \to \infty} \lvert (A + A) \cap [1, N] \rvert / \lvert A \cap [1, N] \rvert \ge 3\).

def sumsetRatioLimsupAtLeastThree : Prop :=
  ∀ A : Set ℕ, A.Infinite →
    Tendsto (fun N : ℕ => ((A ∩ Set.Icc 1 N).ncard : ℝ) / N) atTop (𝓝 0) →
    ∀ ε : ℝ, 0 < ε → ∃ᶠ N : ℕ in atTop,
      (3 - ε) * (A ∩ Set.Icc 1 N).ncard < ((A + A) ∩ Set.Icc 1 N).ncard

Used by 1

Used byFreiman's theorem on sumsets of sets of density zero

TheoremFreiman's theorem on sumsets of sets of density zero#●ready to prove

For \(N \in \mathbb{N}\) write \([1, N] = \{1, \dots, N\}\), and for \(A \subseteq \mathbb{N}\) write \(A + A = \{a + b \mid a, b \in A\}\). Let \(A \subseteq \mathbb{N}\) be an infinite set with \(\lvert A \cap [1, N] \rvert / N \to 0\) as \(N \to \infty\). Then for every real \(\varepsilon > 0\) there are infinitely many \(N\) with \(\lvert (A + A) \cap [1, N] \rvert > (3 - \varepsilon) \lvert A \cap [1, N] \rvert\); that is, \(\limsup_{N \to \infty} \lvert (A + A) \cap [1, N] \rvert / \lvert A \cap [1, N] \rvert \ge 3\).

public theorem_wanted sumsetRatioLimsupAtLeastThree_holds : sumsetRatioLimsupAtLeastThree

Sources

• T. F. Bloom, Erdős Problems, Problem #245, https://www.erdosproblems.com/245 (status PROVED); resolution: G. A. Freiman, Foundations of a structural theory of set addition, Transl. Math. Monogr. 37, Amer. Math. Soc. (1973), erdosproblems.com/245: proved by Freiman [Fr73], https://doi.org/10.1090/mmono/037.

Uses 1

Statement usesErdős Problem 245 on sumsets of sets of density zero

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.