Documentation

Mathlib.Combinatorics.Schnirelmann

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 #

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 #

References #

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
Instances For
    theorem schnirelmannDensity_le_div {A : Set } [DecidablePred fun (x : ) => x A] {n : } (hn : n 0) :
    schnirelmannDensity A (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).card / n
    theorem schnirelmannDensity_mul_le_card_filter {A : Set } [DecidablePred fun (x : ) => x A] {n : } :
    schnirelmannDensity A * n (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).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 : (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).card / n 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_of_not_mem {A : Set } [DecidablePred fun (x : ) => x A] {k : } (hk : kA) :

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

    theorem schnirelmannDensity_eq_zero_of_one_not_mem {A : Set } [DecidablePred fun (x : ) => x A] (h : 1A) :

    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) :

    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.

    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 < nx (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).card / n
    theorem schnirelmannDensity_lt_iff {A : Set } [DecidablePred fun (x : ) => x A] {x : } :
    schnirelmannDensity A < x ∃ (n : ), 0 < n (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).card / n < x
    theorem schnirelmannDensity_le_iff_forall {A : Set } [DecidablePred fun (x : ) => x A] {x : } :
    schnirelmannDensity A x ∀ (ε : ), 0 < ε∃ (n : ), 0 < n (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).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) :
    @[simp]

    The Schnirelmann density is unaffected by adding 0.

    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) :
    theorem exists_of_schnirelmannDensity_eq_zero {A : Set } [DecidablePred fun (x : ) => x A] {ε : } (hε : 0 < ε) (hA : schnirelmannDensity A = 0) :
    ∃ (n : ), 0 < n (Finset.filter (fun (x : ) => x A) (Finset.Ioc 0 n)).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}ᶜ.

    The Schnirelmann density of any finset is 0.

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

    The Schnirelmann density of any finite set is 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.