WeakPNT

@[blueprint  (title := "WeakPNT")  (statement := /--    We have  $$ \sum_{n \leq x} \Lambda(n) = x + o(x).$$  -/)  (proof := /-- Already done by Stoll, assuming Wiener-Ikehara. -/)]theorem WeakPNT : Tendsto (fun N ↦ cumsum Λ N / N) atTop (𝓝 1) := by  let F := vonMangoldt.LFunctionResidueClassAux (q := 1) 1  have hnv := riemannZeta_ne_zero_of_one_le_re  have l1 (n : ℕ) : 0 ≤ Λ n := vonMangoldt_nonneg  have l2 s (hs : 1 < s.re) : F s = LSeries Λ s - 1 / (s - 1) := by    have := vonMangoldt.eqOn_LFunctionResidueClassAux (q := 1) isUnit_one hs    simp only [F, this, vonMangoldt.residueClass, Nat.totient_one, Nat.cast_one, inv_one, one_div, sub_left_inj]    apply LSeries_congr    intro n _    simp only [ofReal_inj, indicator_apply_eq_self, mem_setOf_eq]    exact fun hn ↦ absurd (Subsingleton.eq_one _) hn  have l3 : ContinuousOn F {s | 1 ≤ s.re} := vonMangoldt.continuousOn_LFunctionResidueClassAux 1  have l4 : cheby Λ := vonMangoldt_cheby  have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by    simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm  apply WienerIkeharaTheorem' l1 l5 l4 l3 l2