refine tendsto_tsum_of_dominated_convergence (limiting_fourier_lim1_aux hcheby hx C this) (fun n => ?_) ?_
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
case intro.refine_1
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun x_1 => term f (↑x_1) n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))

case intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    ∀ (k : ℕ),
      ‖term f (↑n) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))