integral_univ_inv_one_add_sq — Mathlib

English

The integral of x ↦ (1+x^2)^{-1} over the real line equals π.

Русский

Интеграл по всей оси f(x) = 1/(1+x^2) равен π.

LaTeX

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

Lean4

@[simp]
theorem integral_univ_inv_one_add_sq : ∫ (x : ℝ), (1 + x ^ 2)⁻¹ = π :=
  (by ring : π = (π / 2) - (-(π / 2))) ▸
    integral_of_hasDerivAt_of_tendsto hasDerivAt_arctan' integrable_inv_one_add_sq
      (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atBot)
      (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atTop)

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