English
The Schnirelmann density of any finite set is 0.
Русский
Плотность Шниррельмана любого конечного множества равна 0.
LaTeX
$$schnirelmannDensity( A ) = 0$$
Lean4
/-- The Schnirelmann density of any finset is `0`. -/
theorem schnirelmannDensity_finset (A : Finset ℕ) : schnirelmannDensity A = 0 :=
by
refine le_antisymm ?_ schnirelmannDensity_nonneg
simp only [schnirelmannDensity_le_iff_forall, zero_add]
intro ε hε
wlog hε₁ : ε ≤ 1 generalizing ε
· obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl
exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩
let n : ℕ := ⌊#A / ε⌋₊ + 1
have hn : 0 < n := Nat.succ_pos _
use n, hn
rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one]
exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff]
