English
If k ∉ A, then schnirelmannDensity(A) ≤ 1 − k^{-1}.
Русский
Если k не принадлежит A, то плотность Шнирельмана не превосходит 1 − k^{-1}.
LaTeX
$$$ k \\notin A \\Rightarrow \\operatorname{schnirelmanDensity}(A) \\le 1 - (k^{-1} : \\mathbb{R}) $$$
Lean4
/-- If `k` is omitted from the set, its Schnirelmann density is upper bounded by `1 - k⁻¹`.
-/
theorem schnirelmannDensity_le_of_notMem {k : ℕ} (hk : k ∉ A) : schnirelmannDensity A ≤ 1 - (k⁻¹ : ℝ) :=
by
rcases k.eq_zero_or_pos with rfl | hk'
· simpa using schnirelmannDensity_le_one
apply schnirelmannDensity_le_of_le k hk'.ne'
rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']
gcongr
rw [← Nat.cast_pred hk', Nat.cast_le]
suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
rw [← Ioo_insert_right hk', filter_insert, if_neg hk]
exact filter_subset _ _
