WeakPNT_AP_prelim

@[blueprint "WeakPNT-AP-prelim"  (title := "WeakPNT-AP-prelim")  (statement := /--  If $q ≥ 1$ and $a$ is coprime to $q$, the Dirichlet series  $\sum_{n \leq x: n = a\ (q)} \frac{\Lambda(n)}{n^s}$ converges for $\mathrm{Re}(s) > 1$ to  $\frac{1}{\varphi(q)} \frac{1}{s-1} + G(s)$ where $G$ has a continuous extension to  $\mathrm{Re}(s)=1$.  -/)  (proof := /--  We expand out the left-hand side using Lemma \ref{WeakPNT-character}.  The contribution of the  non-principal characters $\chi$ extend continuously to $\mathrm{Re}(s) = 1$ thanks to the  non-vanishing of $L(s,\chi)$ on this line (which should follow from another component of  this project), so it suffices to show that for the principal character $\chi_0$, that  $$ -\frac{L'(s,\chi_0)}{L(s,\chi_0)} - \frac{1}{s-1}$$  also extends continuously here.  But we already know that  $$ -\frac{\zeta'(s)}{\zeta(s)} - \frac{1}{s-1}$$  extends, and from Euler product machinery one has the identity  $$ \frac{L'(s,\chi_0)}{L(s,\chi_0)}  = \frac{\zeta'(s)}{\zeta(s)} + \sum_{p|q} \frac{\log p}{p^s-1}.$$  Since there are only finitely many primes dividing $q$, and each summand $\frac{\log p}{p^s-1}$  extends continuously, the claim follows.  -/)  (proofUses := ["ChebyshevPsi", "WeakPNT-character"])  (latexEnv := "proposition")]theorem WeakPNT_AP_prelim {q : ℕ} {a : ℕ} (hq : q ≥ 1) (ha : Nat.Coprime a q) (ha' : a < q) :    ∃ G: ℂ → ℂ, (ContinuousOn G {s | 1 ≤ s.re}) ∧    (Set.EqOn G (fun s ↦ LSeries (fun n ↦ if n % q = a then Λ n else 0) s - 1 /      ((Nat.totient q) * (s - 1))) {s | 1 < s.re}) := by  have : NeZero q := NeZero.of_pos hq  have hG : ∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧ Set.EqOn G      (fun s ↦ LSeries (fun n ↦ if (n : ZMod q) = a then Λ n else 0) s - (q.totient : ℂ)⁻¹ / (s - 1)) {s | 1 < s.re} := by    use vonMangoldt.LFunctionResidueClassAux (a : ZMod q), vonMangoldt.continuousOn_LFunctionResidueClassAux (q := q) (a := a)    have := vonMangoldt.eqOn_LFunctionResidueClassAux ((ZMod.isUnit_iff_coprime a q).mpr ha)    convert this using 6; split <;> simp_all  convert hG using 6  · simp [ZMod.natCast_eq_natCast_iff', Nat.mod_eq_of_lt ha']  · rw [inv_eq_one_div, div_div]