English
The series summing 1/n over primes in the residue class a mod q diverges; in particular there are infinitely many such primes.
Русский
Ряд, суммающийся по 1/n только по простым n, удовлетворяющим n ≡ a (mod q), расходится; следовательно таких простых бесконечно много.
LaTeX
$$$\\neg \\operatorname{Summable}\\!\\big( \\lambda n. \\frac{\\mathbf{1}_{\\text{Prime}(n) \\land n \\equiv a\\,(q)}}{n} \\big) $$$
Lean4
/-- The function `n ↦ Λ n / n` restricted to primes in an invertible residue class
is not summable. This then implies that there must be infinitely many such primes. -/
theorem not_summable_residueClass_prime_div (ha : IsUnit a) :
¬Summable fun n : ℕ ↦ (if n.Prime then residueClass a n else 0) / n :=
by
intro H
have key : Summable fun n : ℕ ↦ residueClass a n / n :=
by
convert (summable_residueClass_non_primes_div a).add H using 2 with n
simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]
let C := ∑' n, residueClass a n / n
have H₁ {x : ℝ} (hx : 1 < x) : ∑' n, residueClass a n / (n : ℝ) ^ x ≤ C :=
by
refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key
· rcases n.eq_zero_or_pos with rfl | hn
· simp only [Nat.cast_zero, Real.zero_rpow (zero_lt_one.trans hx).ne', div_zero, le_refl]
· refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
conv_lhs => rw [← Real.rpow_one n]
exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le
· exact summable_real_of_abscissaOfAbsConv_lt <| (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| mod_cast hx
obtain ⟨C', hC'⟩ := LSeries_residueClass_lower_bound ha
have H₁ {x} (hx : x ∈ Set.Ioc 1 2) : (q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1) :=
(div_le_iff₀ <| sub_pos.mpr hx.1).mp <| sub_le_iff_le_add.mp <| (hC' hx).trans (H₁ hx.1)
have hq : 0 < (q.totient : ℝ)⁻¹ := inv_pos.mpr (mod_cast q.totient.pos_of_neZero)
rcases le_or_gt (C + C') 0 with h₀ | h₀
· have := hq.trans_le (H₁ (Set.right_mem_Ioc.mpr one_lt_two))
rw [show (2 : ℝ) - 1 = 1 by norm_num, mul_one] at this
exact (this.trans_le h₀).false
· obtain ⟨ξ, hξ₁, hξ₂⟩ : ∃ ξ ∈ Set.Ioc 1 2, (C + C') * (ξ - 1) < (q.totient : ℝ)⁻¹ :=
by
refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
·
simpa only [lt_inf_iff, lt_add_iff_pos_right, Nat.ofNat_pos, div_pos_iff_of_pos_right, Nat.one_lt_ofNat,
and_true] using div_pos hq h₀
· rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]
exact (min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two
exact ((H₁ hξ₁).trans_lt hξ₂).false
