have l2 : IntegrableOn (fun i ↦ W21.norm ψ * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-Real.log x)) := by
  exact (l3.const_mul _).integrableOn
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)