Theorems · Theorem · number theory

exists_of_schnirelmannDensity_eq_zero

∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {ε : ℝ},
  0 < ε → 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}ᶜ.

Defined in

Mathlib.Combinatorics.Schnirelmann

Cited by

0 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePred