have key := (continuous_re.tendsto _).comp (@wiener_ikehara_smooth' A Ψ G f hf hcheby hG hG' l1 l2 l3)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
Ψ : ℝ → ℝ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
Ψ : ℝ → ℝ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
key :
  Tendsto (re ∘ fun x => (∑' (n : ℕ), (fun n => ↑(f n)) n * (fun n => ↑(Ψ n)) (↑n / x)) / ↑x) atTop
    (𝓝 (↑A * ∫ (y : ℝ) in Ioi 0, (fun n => ↑(Ψ n)) y).re)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))