schnirelmannDensity_mul_le_card_filter

English

For any A ⊆ ℕ and n ∈ ℕ, schnirelmannDensity(A) · n ≤ |{a ∈ Ioc 0 n | a ∈ A}|.

Русский

Для любого A ⊆ ℕ и n: плотность Шнирельмана, умноженная на n, не превосходит число элементов A в {1, ..., n}.

LaTeX

$$$ \\operatorname{schnirelmanDensity}(A) \\cdot n \\le \\#\\{ a \\in Ioc 0 n \\mid a \\in A \\} $$$

Lean4

/-- For any natural `n`, the Schnirelmann density multiplied by `n` is bounded by `|A ∩ {1, ..., n}|`.
Note this property fails for the natural density.
-/
theorem schnirelmannDensity_mul_le_card_filter {n : ℕ} : schnirelmannDensity A * n ≤ #({a ∈ Ioc 0 n | a ∈ A}) :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

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