English
The Schnirelmann density of a set A ⊆ ℕ is the infimum over n of the ratio |A ∩ {1, ..., n}| / n, taken over n > 0.
Русский
Плотность Шнирельмана множества A ⊆ ℕ определяется как infimum отношения |A ∩ {1, ..., n}| / n по всем n > 0.
LaTeX
$$$ \\operatorname{schnirelmannDensity}(A) = \\inf_{n > 0} \\frac{\\#\\{ a \\in Ioc 0 n \\mid a \\in A \\}}{n} $$$
Lean4
/-- The Schnirelmann density is defined as the infimum of |A ∩ {1, ..., n}| / n as n ranges over
the positive naturals. -/
noncomputable def schnirelmannDensity (A : Set ℕ) [DecidablePred (· ∈ A)] : ℝ :=
⨅ n : { n : ℕ // 0 < n }, #({a ∈ Ioc 0 n | a ∈ A}) / n