English
The Schnirelmann density of {n | n ≡ 1 (mod m)} equals m^{-1} for m ≠ 1.
Русский
Плотность множества {n | n ≡ 1 (mod m)} равна m^{-1} при m ≠ 1.
LaTeX
$$\\forall m \\neq 1, \\operatorname{schnirelmannDensity}({n \\mid n \\equiv 1 \\\\[MOD m]}) = m^{-1}$$
Lean4
/-- The Schnirelmann density of the set of naturals which are `1 mod m` is `m⁻¹`, for any `m ≠ 1`.
Note that if `m = 1`, this set is empty.
-/
theorem schnirelmannDensity_setOf_mod_eq_one {m : ℕ} (hm : m ≠ 1) : schnirelmannDensity {n | n % m = 1} = (m⁻¹ : ℝ) :=
by
rcases m.eq_zero_or_pos with rfl | hm'
· simp only [Nat.cast_zero, inv_zero]
refine schnirelmannDensity_finite ?_
simp
apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _
· rw [← one_div, ← @Nat.cast_one ℝ]
gcongr
simp only [Set.mem_setOf_eq, card_le_one_iff_subset_singleton, subset_iff, mem_filter, mem_Ioc, mem_singleton,
and_imp]
use 1
intro x _ hxm h
rcases eq_or_lt_of_le hxm with rfl | hxm'
· simp at h
rwa [Nat.mod_eq_of_lt hxm'] at h
rw [le_schnirelmannDensity_iff]
intro n hn
simp only [Set.mem_setOf_eq]
have : (Icc 0 ((n - 1) / m)).image (· * m + 1) ⊆ {x ∈ Ioc 0 n | x % m = 1} :=
by
simp only [subset_iff, mem_image, forall_exists_index, mem_filter, mem_Ioc, mem_Icc, and_imp]
rintro _ y _ hy' rfl
have hm : 2 ≤ m := hm.lt_of_le' hm'
simp only [Nat.mul_add_mod', Nat.mod_eq_of_lt hm, add_pos_iff, or_true, and_true, true_and,
← Nat.le_sub_iff_add_le hn, zero_lt_one]
exact Nat.mul_le_of_le_div _ _ _ hy'
rw [le_div_iff₀ (Nat.cast_pos.2 hn), mul_comm, ← div_eq_mul_inv]
apply (Nat.cast_le.2 (card_le_card this)).trans'
rw [card_image_of_injective, Nat.card_Icc, Nat.sub_zero, div_le_iff₀ (Nat.cast_pos.2 hm'), ← Nat.cast_mul,
Nat.cast_le, add_one_mul (α := ℕ)]
· have := @Nat.lt_div_mul_add n.pred m hm'
rwa [← Nat.succ_le, Nat.succ_pred hn.ne'] at this
intro a b
simp [hm'.ne']
