exact (((integrable_inv_one_add_sq.comp_div (by simp [pi_ne_zero])).const_mul _).const_mul _).restrict
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C * (1 + (t / (2 * π)) ^ 2)⁻¹)) (volume.restrict (Ici (-x.log)))
no goals