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
andschnirelmannDensity_le_one
. schnirelmannDensity_le_of_not_mem
: Ifk ∉ A
, the density can be easily upper-bounded by1 - 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 #
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 }), ↑(Finset.filter (fun (x : ℕ) => x ∈ A) (Finset.Ioc 0 ↑n)).card / ↑↑n
Instances For
For any natural n
, the Schnirelmann density multiplied by n
is bounded by |A ∩ {1, ..., n}|
.
Note this property fails for the natural density.
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
.
If k
is omitted from the set, its Schnirelmann density is upper bounded by 1 - k⁻¹
.
The Schnirelmann density of a set not containing 1
is 0
.
The Schnirelmann density is increasing with the set.
The Schnirelmann density of A
is 1
if and only if A
contains all the positive naturals.
The Schnirelmann density of A
containing 0
is 1
if and only if A
is the naturals.
The Schnirelmann density is unaffected by adding 0
.
The Schnirelmann density is unaffected by removing 0
.
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}ᶜ
.
The Schnirelmann density of any finset is 0
.
The Schnirelmann density of any finite set is 0
.
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.