integrable_inv_one_add_sq — Mathlib

English

The function x ↦ (1+x^2)^{-1} is integrable on all of ℝ (Lebesgue measure).

Русский

Функция x ↦ (1+x^2)^{-1} интегрируема по Лебегу на всей ℝ.

LaTeX

$$$\int_{-\infty}^{\infty} \frac{dx}{1+x^{2}} < \infty$$$

Lean4

theorem integrable_inv_one_add_sq : Integrable fun (x : ℝ) ↦ (1 + x ^ 2)⁻¹ :=
  by
  suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]
  exact integrable_rpow_neg_one_add_norm_sq (by simp)

Похожие утверждения