Schnirelmann density

TheoremSchnirelmann's inequality#✓fully proved

For a set \(A\) of natural numbers, let \(\sigma(A) = \inf_{n \ge 1} |A \cap \{1, \dots, n\}| / n\) be its Schnirelmann density. If \(A\) and \(B\) are sets of natural numbers that both contain \(0\), then their sumset \(A + B = \{a + b : a \in A,\ b \in B\}\) satisfies \(\sigma(A) + \sigma(B) - \sigma(A)\sigma(B) \le \sigma(A + B)\).

theorem _root_.schnirelmannDensity_add_lower_bound {A B : Set ℕ}
    [DecidablePred (· ∈ A)] [DecidablePred (· ∈ B)] [DecidablePred (· ∈ A + B)]
    (hA : 0 ∈ A) (hB : 0 ∈ B) :
    schnirelmannDensity A + schnirelmannDensity B -
        schnirelmannDensity A * schnirelmannDensity B ≤
      schnirelmannDensity (A + B)

Used by 1

Used bySchnirelmann's basis theorem

TheoremSchnirelmann's basis theorem#✓fully proved

Let \(A\) be a set of natural numbers with \(0 \in A\) whose Schnirelmann density \(\sigma(A) = \inf_{n \ge 1} |A \cap \{1, \dots, n\}| / n\) is positive. Then \(A\) is an additive basis of finite order: there is a natural number \(h\) such that every natural number \(n\) can be written as \(n = a_1 + \dots + a_h\) with \(a_1, \dots, a_h \in A\), repetitions allowed.

theorem _root_.exists_additive_basis_of_pos_schnirelmannDensity {A : Set ℕ}
    [DecidablePred (· ∈ A)] (hA : 0 ∈ A) (hσ : 0 < schnirelmannDensity A) :
    ∃ h : ℕ, ∀ n : ℕ, ∃ x : Fin h → ℕ,
      (∀ i, x i ∈ A) ∧ n = ∑ i, x i

Sources

• Lemma 1 of Tim Jameson's notes on Linnik's proof of the Waring-Hilbert theorem.

Uses 1 · Used by 1

Proof usesSchnirelmann's inequality

Used byHilbert–Waring theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.