norm_cast
case h.e_a
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ici (-x.log), cexp (2 * ↑π * (↑u / (2 * ↑π))) * Ψ (rexp (2 * π * (u / (2 * π)))) =
    ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
case h.e_a
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (2 * π * (u / (2 * π)))) * Ψ (rexp (2 * π * (u / (2 * π)))) =
    ∫ (y : ℝ) in Ioi x⁻¹, Ψ y