poisson_kernel_integrable

theorem poisson_kernel_integrable (x : ℝ) (hx : x ≠ 0) :  MeasureTheory.Integrable (fun (t : ℝ) ↦ (‖x + t * I‖^2)⁻¹) := by  -- First, simplify the complex norm  have h1 : ∀ t : ℝ, ‖x + t * I‖^2 = x^2 + t^2 := by    intro t    rw [← normSq_eq_norm_sq, normSq_add_mul_I]  -- Rewrite the integrand using this simplification  simp_rw [h1]  apply integrable_comp_mul_left_iff _ hx |>.mp  have : (fun t ↦ (x ^ 2 + (x * t) ^ 2) ⁻¹) = (fun t ↦ (1 / x ^ 2) * (1 + t ^ 2) ⁻¹) := by    ext    field_simp  rw [this]  apply integrable_inv_one_add_sq.const_mul