WeakPNT_AP

@[blueprint "WeakPNT-AP"  (title := "WeakPNT-AP")  (statement := /--  If $q ≥ 1$ and $a$ is coprime to $q$, we have  $$ \sum_{n \leq x: n = a\ (q)} \Lambda(n) = \frac{x}{\varphi(q)} + o(x).$$  -/)  (proof := /-- Apply Theorem \ref{WienerIkehara} (or Theorem \ref{WienerIkehara2} to avoid  checking the Chebyshev condition) using Proposition \ref{WeakPNT-AP-prelim}.-/)  (proofUses := ["WienerIkehara", "WeakPNT-AP-prelim"])]theorem WeakPNT_AP {q : ℕ} {a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) :    Tendsto (fun N ↦ cumsum (fun n ↦ if n % q = a then Λ n else 0) N / N) atTop (𝓝 (1 / q.totient)) := by  have h_summable : ∀ s : ℝ, 1 < s → Summable (fun n ↦ (if n % q = a then Λ n else 0) / n ^ s) := by    intro s hs    refine .of_nonneg_of_le (fun n ↦ ?_) (fun n ↦ ?_) (summable_vonMangoldt_div_rpow hs)    · split_ifs <;> positivity    · split_ifs <;> norm_num; exact div_nonneg vonMangoldt_nonneg (by positivity)  obtain ⟨G, hG₁, hG₂⟩ := WeakPNT_AP_prelim hq ha ha'  convert WienerIkeharaTheorem'' _ _ _ _ using 1  · use G  · intro n    simp_all only [ge_iff_le, one_div, mul_inv_rev, Pi.ofNat_apply]    split    next h => subst h; simp_all only [vonMangoldt_nonneg]    next h => simp_all only [le_refl]  · intro σ' hσ'    specialize h_summable σ' hσ'    simp_all only [ge_iff_le, one_div, mul_inv_rev]    convert h_summable using 1    ext    simp only [nterm, norm_real, norm_eq_abs]    ring_nf    split_ifs <;> simp [*, mul_comm]  · assumption  · convert hG₂ using 3    · exact tsum_congr fun n ↦ by cases n <;> aesop    · norm_num [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]