English
If the Schnirelmann density of A is 0, then for every positive ε there exists n with |A ∩ {1,...,n}|/n < ε.
Русский
Если плотность Шниррельмана A равна 0, то для каждого положительного ε существует n такое, что |A ∩ {1,...,n}|/n < ε.
LaTeX
$$0 < ε ∧ schnirelmannDensity(A) = 0 \\Rightarrow ∃ n > 0, \\frac{\\#\\left\\{a ∈ Ioc 0 n \\mid a ∈ A\\right\\}}{n} < ε$$
Lean4
/-- 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}ᶜ`.
-/
theorem exists_of_schnirelmannDensity_eq_zero {ε : ℝ} (hε : 0 < ε) (hA : schnirelmannDensity A = 0) :
∃ n, 0 < n ∧ #({a ∈ Ioc 0 n | a ∈ A}) / n < ε := by
by_contra! h
rw [← le_schnirelmannDensity_iff] at h
linarith
