refine tendsto_integral_filter_of_dominated_convergence _ ?_ ?_ (limiting_fourier_lim2_aux x C) ?_
case intro.hg
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun x_1 => ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (𝓝[>] 1)
    (𝓝 (∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
case intro.hg.refine_1
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    AEStronglyMeasurable (fun u => ↑(rexp (-u * (n - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))

case intro.hg.refine_2
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
      ‖↑(rexp (-a * (n - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))

case intro.hg.refine_3
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
    Tendsto (fun n => ↑(rexp (-a * (n - 1))) * 𝓕 ψ.toFun (a / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (a / (2 * π))))