schnirelmannDensity — Mathlib

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

Похожие утверждения