Schnirelmann density

We define the Schnirelmann density of a set A of natural numbers as $inf_{n > 0} |A ∩ {1,...,n}| / n$. As this density is very sensitive to changes in small values, we must exclude 0 from the infimum, and from the intersection.

Main statements

• Simple bounds on the Schnirelmann density, that it is between 0 and 1 are given in schnirelmannDensity_nonneg and schnirelmannDensity_le_one.
• schnirelmannDensity_le_of_notMem: If k ∉ A, the density can be easily upper-bounded by 1 - k⁻¹

Implementation notes

Despite the definition being noncomputable, we include a decidable instance argument, since this makes the definition easier to use in explicit cases. Further, we use Finset.Ioc rather than a set intersection since the set is finite by construction, which reduces the proof obligations later that would arise with Nat.card.

TODO

• Give other calculations of the density, for example powers and their sumsets.
• Define other densities like the lower and upper asymptotic density, and the natural density, and show how these relate to the Schnirelmann density.
• Show that if the sum of two densities is at least one, the sumset covers the positive naturals.
• Prove Schnirelmann's theorem and Mann's theorem on the subadditivity of this density.

References

• [Ruzsa, Imre, Sumsets and structure][ruzsa2009]

noncomputable def schnirelmannDensity (A : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ A] : ℝ

The Schnirelmann density is defined as the infimum of |A ∩ {1, ..., n}| / n as n ranges over the positive naturals.

Equations

• schnirelmannDensity A = ⨅ (n : { n : ℕ // 0 < n }), ↑{a ∈ Finset.Ioc 0 ↑n | a ∈ A}.card / ↑↑n

theorem schnirelmannDensity_nonneg {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] : 0 ≤ schnirelmannDensity A

theorem schnirelmannDensity_le_div {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {n : ℕ} (hn : n ≠ 0) : schnirelmannDensity A ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n

theorem schnirelmannDensity_mul_le_card_filter {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {n : ℕ} : schnirelmannDensity A * ↑n ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card

For any natural n, the Schnirelmann density multiplied by n is bounded by |A ∩ {1, ..., n}|. Note this property fails for the natural density.

theorem schnirelmannDensity_le_of_le {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {x : ℝ} (n : ℕ) (hn : n ≠ 0) (hx : ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n ≤ x) : schnirelmannDensity A ≤ x

To show the Schnirelmann density is upper bounded by x, it suffices to show |A ∩ {1, ..., n}| / n ≤ x, for any chosen positive value of n.

We provide n explicitly here to make this lemma more easily usable in apply or refine. This lemma is analogous to ciInf_le_of_le.

theorem schnirelmannDensity_le_one {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] : schnirelmannDensity A ≤ 1

theorem schnirelmannDensity_le_of_notMem {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {k : ℕ} (hk : k ∉ A) : schnirelmannDensity A ≤ 1 - (↑k)⁻¹

If k is omitted from the set, its Schnirelmann density is upper bounded by 1 - k⁻¹.

@[deprecated schnirelmannDensity_le_of_notMem (since := "2025-05-23")]

theorem schnirelmannDensity_le_of_not_mem {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {k : ℕ} (hk : k ∉ A) : schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Alias of schnirelmannDensity_le_of_notMem.

---

If k is omitted from the set, its Schnirelmann density is upper bounded by 1 - k⁻¹.

theorem schnirelmannDensity_eq_zero_of_one_notMem {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] (h : 1 ∉ A) : schnirelmannDensity A = 0

The Schnirelmann density of a set not containing 1 is 0.

@[deprecated schnirelmannDensity_eq_zero_of_one_notMem (since := "2025-05-23")]

theorem schnirelmannDensity_eq_zero_of_one_not_mem {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] (h : 1 ∉ A) : schnirelmannDensity A = 0

Alias of schnirelmannDensity_eq_zero_of_one_notMem.

---

The Schnirelmann density of a set not containing 1 is 0.

theorem schnirelmannDensity_le_of_subset {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {B : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ B] (h : A ⊆ B) : schnirelmannDensity A ≤ schnirelmannDensity B

The Schnirelmann density is increasing with the set.

theorem schnirelmannDensity_eq_one_iff {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

The Schnirelmann density of A is 1 if and only if A contains all the positive naturals.

theorem schnirelmannDensity_eq_one_iff_of_zero_mem {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] (hA : 0 ∈ A) : schnirelmannDensity A = 1 ↔ A = Set.univ

The Schnirelmann density of A containing 0 is 1 if and only if A is the naturals.

theorem le_schnirelmannDensity_iff {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {x : ℝ} : x ≤ schnirelmannDensity A ↔ ∀ (n : ℕ), 0 < n → x ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n

theorem schnirelmannDensity_lt_iff {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {x : ℝ} : schnirelmannDensity A < x ↔ ∃ (n : ℕ), 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < x

theorem schnirelmannDensity_le_iff_forall {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {x : ℝ} : schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < x + ε

theorem schnirelmannDensity_congr' {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {B : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ B] (h : ∀ n > 0, n ∈ A ↔ n ∈ B) : schnirelmannDensity A = schnirelmannDensity B

@[simp]

theorem schnirelmannDensity_insert_zero {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] [DecidablePred fun (x : ℕ) => x ∈ insert 0 A] : schnirelmannDensity (insert 0 A) = schnirelmannDensity A

The Schnirelmann density is unaffected by adding 0.

theorem schnirelmannDensity_diff_singleton_zero {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] [DecidablePred fun (x : ℕ) => x ∈ A \ {0}] : schnirelmannDensity (A \ {0}) = schnirelmannDensity A

The Schnirelmann density is unaffected by removing 0.

theorem schnirelmannDensity_congr {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {B : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ B] (h : A = B) : schnirelmannDensity A = schnirelmannDensity B

theorem exists_of_schnirelmannDensity_eq_zero {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] {ε : ℝ} (hε : 0 < ε) (hA : schnirelmannDensity A = 0) : ∃ (n : ℕ), 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < ε

If the Schnirelmann density is 0, there is a positive natural for which |A ∩ {1, ..., n}| / n < ε, for any positive ε. Note this cannot be improved to ∃ᶠ n : ℕ in atTop, as can be seen by A = {1}ᶜ.

@[simp]

theorem schnirelmannDensity_empty : schnirelmannDensity ∅ = 0

theorem schnirelmannDensity_finset (A : Finset ℕ) : schnirelmannDensity ↑A = 0

The Schnirelmann density of any finset is 0.

theorem schnirelmannDensity_finite {A : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] (hA : A.Finite) : schnirelmannDensity A = 0

The Schnirelmann density of any finite set is 0.

@[simp]

theorem schnirelmannDensity_univ : schnirelmannDensity Set.univ = 1

theorem schnirelmannDensity_setOf_even : schnirelmannDensity (setOf Even) = 0

theorem schnirelmannDensity_setOf_prime : schnirelmannDensity (setOf Nat.Prime) = 0

theorem schnirelmannDensity_setOf_mod_eq_one {m : ℕ} (hm : m ≠ 1) : schnirelmannDensity {n : ℕ | n % m = 1} = (↑m)⁻¹

The Schnirelmann density of the set of naturals which are 1 mod m is m⁻¹, for any m ≠ 1.

Note that if m = 1, this set is empty.

theorem schnirelmannDensity_setOf_modeq_one {m : ℕ} : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m)⁻¹

theorem schnirelmannDensity_setOf_Odd : schnirelmannDensity (setOf Odd) = 2⁻¹