integral_Ioi_inv_one_add_sq — Mathlib

English

For real i, the improper integral from i to ∞ of 1/(1+x^2) dx equals π/2 − arctan(i).

Русский

Для вещественного i, неопределённый интеграл от i до ∞ дроби 1/(1+x^2) dx равен π/2 − arctan(i).

LaTeX

$$$\int_{i}^{\infty} \frac{dx}{1+x^{2}} = \frac{\pi}{2} - \arctan(i), \quad i\in\mathbb{R}$$$

Lean4

@[simp]
theorem integral_Ioi_inv_one_add_sq {i : ℝ} : ∫ (x : ℝ) in Set.Ioi i, (1 + x ^ 2)⁻¹ = (π / 2) - arctan i :=
  integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => hasDerivAt_arctan' x) integrable_inv_one_add_sq.integrableOn
    (tendsto_nhds_of_tendsto_nhdsWithin tendsto_arctan_atTop)

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