English
The series n ↦ (if n is prime then 0 else residueClass a n)/n is summable; this follows by comparing with vonMangoldt and using nonnegativity arguments.
Русский
Членов ряда n ↦ (если n простое, то 0, иначе residueClass a n)/n суммируемы; это следует из сравнения с vonMangoldt и неотрицательности.
LaTeX
$$$\sum_{n} \frac{\operatorname{residueClass}(a;n)\mathbf{1}_{\lnot \text{Prime}}(n)}{n} < \infty$$$
Lean4
/-- The function `n ↦ Λ n / n`, restricted to non-primes in a residue class, is summable.
This is used to convert results on `ArithmeticFunction.vonMangoldt.residueClass` to results
on primes in an arithmetic progression. -/
theorem summable_residueClass_non_primes_div : Summable fun n : ℕ ↦ (if n.Prime then 0 else residueClass a n) / n :=
by
have h₀ (n : ℕ) : 0 ≤ (if n.Prime then 0 else residueClass a n) / n :=
by
have := residueClass_nonneg a n
positivity
have hleF₀ (n : ℕ) : (if n.Prime then 0 else residueClass a n) / n ≤ F₀ n :=
by
refine div_le_div_of_nonneg_right ?_ n.cast_nonneg
split_ifs; exacts [le_rfl, residueClass_le a n]
refine Summable.of_nonneg_of_le h₀ hleF₀ ?_
have hF₀ (p : Nat.Primes) : F₀ p.val = 0 := by simp only [p.prop, ↓reduceIte, zero_div, F₀]
refine
(summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr fun n ↦
Set.indicator_apply_eq_self.mpr fun (hn : ¬IsPrimePow n) ↦ ?_
swap
·
simp +contextual only [div_eq_zero_iff, ite_eq_left_iff, vonMangoldt_eq_zero_iff, hn, not_false_eq_true,
implies_true, Nat.cast_eq_zero, true_or, F₀]
have hFF' : F₀ ∘ Subtype.val (p := fun n ↦ n ∈ {n | IsPrimePow n}) = F' ∘ ⇑prodNatEquiv.symm :=
by
refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_
ext1 n
simp only [Function.comp_apply, F']
congr
rw [hFF']
refine (Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_
have hF'₀ (p : Nat.Primes) : F' (p, 0) = 0 := by simp only [zero_add, pow_one, hF₀, F']
have hF'₁ : F'' = F' ∘ (Prod.map _root_.id (· + 1)) := by
ext1
simp only [Function.comp_apply, Prod.map_fst, id_eq, Prod.map_snd, F'', F']
refine (Function.Injective.summable_iff ?_ fun u hu ↦ ?_).mp <| hF'₁ ▸ summable_F''
· exact Function.Injective.prodMap (fun ⦃a₁ a₂⦄ a ↦ a) <| add_left_injective 1
· simp only [Set.range_prodMap, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range, Nat.exists_add_one_eq,
true_and, not_lt, nonpos_iff_eq_zero] at hu
rw [← hF'₀ u.1, ← hu]
