English
If there exists n with n ≠ 0 and (# {a ∈ Ioc 0 n | a ∈ A}) / n ≤ x, then schnirelmannDensity(A) ≤ x.
Русский
Если существует n ≠ 0 такое, что доля элементов A в {1, ..., n} не превышает x, то плотность Шнирельмана не превышает x.
LaTeX
$$$ \\exists n, n \\neq 0 \\land \\frac{\\#\\{ a \\in Ioc 0 n \\mid a \\in A \\}}{n} \\le x \\;\\Rightarrow\\; \\operatorname{schnirelmanDensity}(A) \\le x $$$
Lean4
/-- 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_le {x : ℝ} (n : ℕ) (hn : n ≠ 0) (hx : #({a ∈ Ioc 0 n | a ∈ A}) / n ≤ x) :
schnirelmannDensity A ≤ x :=
(schnirelmannDensity_le_div hn).trans hx
