WienerIkeharaTheorem'

@[blueprint "WienerIkehara"  (title := "Wiener-Ikehara Theorem (1)")  (statement := /--    We have  $$ \sum_{n\leq x} f(n) = A x + o(x).$$  -/)  (proof := /-- Apply the preceding proposition with $I = [\varepsilon,1]$ and then send  $\varepsilon$ to zero (using \eqref{cheby} to control the error). -/)  (latexEnv := "corollary")]theorem WienerIkeharaTheorem' {f : ℕ → ℝ} (hpos : 0 ≤ f)    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (hcheby : cheby f) (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re}) :    Tendsto (fun N => cumsum f N / N) atTop (𝓝 A) := by   convert_to Tendsto (S f 0) atTop (𝓝 A) ; · ext N ; simp [S, cumsum]  apply (tendsto_S_S_zero hpos hcheby).tendsto_of_eventually_tendsto  · have L0 : Ioc 0 1 ∈ 𝓝[>] (0 : ℝ) := inter_mem_nhdsWithin _ (Iic_mem_nhds zero_lt_one)    apply eventually_of_mem L0    · intro ε hε      simpa using! WienerIkeharaInterval_discrete' hpos hf hcheby hG hG' hε.1 hε.2  · have : Tendsto (fun ε : ℝ => ε) (𝓝[>] 0) (𝓝 0) := nhdsWithin_le_nhds    simpa using (this.const_sub 1).const_mul A