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.
• Prove Schnirelmann's theorem and Mann's theorem on the subadditivity of this density.

References

• Ruzsa, Imre, Sumsets and structure

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⁻¹.

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.

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_sdiff_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.

@[deprecated schnirelmannDensity_sdiff_singleton_zero (since := "2026-06-03")]

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

Alias of schnirelmannDensity_sdiff_singleton_zero.

---

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_setOfPred_even : schnirelmannDensity (Set.ofPred Even) = 0

@[deprecated schnirelmannDensity_setOfPred_even (since := "2026-07-09")]

theorem schnirelmannDensity_setOf_even : schnirelmannDensity (Set.ofPred Even) = 0

Alias of schnirelmannDensity_setOfPred_even.

theorem schnirelmannDensity_setOfPred_prime : schnirelmannDensity (Set.ofPred Nat.Prime) = 0

@[deprecated schnirelmannDensity_setOfPred_prime (since := "2026-07-09")]

theorem schnirelmannDensity_setOf_prime : schnirelmannDensity (Set.ofPred Nat.Prime) = 0

Alias of schnirelmannDensity_setOfPred_prime.

theorem schnirelmannDensity_setOfPred_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.

@[deprecated schnirelmannDensity_setOfPred_mod_eq_one (since := "2026-07-09")]

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

Alias of schnirelmannDensity_setOfPred_mod_eq_one.

---

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_setOfPred_modeq_one {m : ℕ} : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m)⁻¹

@[deprecated schnirelmannDensity_setOfPred_modeq_one (since := "2026-07-09")]

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

Alias of schnirelmannDensity_setOfPred_modeq_one.

theorem schnirelmannDensity_setOfPred_Odd : schnirelmannDensity (Set.ofPred Odd) = 2⁻¹

@[deprecated schnirelmannDensity_setOfPred_Odd (since := "2026-07-09")]

theorem schnirelmannDensity_setOf_Odd : schnirelmannDensity (Set.ofPred Odd) = 2⁻¹

Alias of schnirelmannDensity_setOfPred_Odd.

theorem add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity {A B : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ A] [DecidablePred fun (x : ℕ) => x ∈ B] (hA : 0 ∈ A) (hB : 0 ∈ B) (h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B) : A + B = Set.univ

If two sets A and B have Schnirelmann densities with sum at least 1, and both sets contain zero, then every natural number is sum of an element of A and an element of B. Note that we cannot omit the assumption that both sets contain zero, as shown by the counterexample A = B = Odd.