integral_one_div_one_add_sq — Mathlib

English

For real a ≤ b, ∫_a^b 1/(1+x^2) dx = arctan b − arctan a.

Русский

Для действительных a ≤ b интеграл 1/(1+x^2) по [a,b] равен arctan b − arctan a.

LaTeX

$$$\forall a,b \in \mathbb{R},\ \displaystyle \int_a^b \frac{1}{1+x^2} \, dx = \arctan b - \arctan a$$$

Lean4

theorem integral_one_div_one_add_sq : (∫ x : ℝ in a..b, ↑1 / (↑1 + x ^ 2)) = arctan b - arctan a :=
  by
  refine
    integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
      (continuous_const.div ?_ fun x => ?_).continuousOn
  · fun_prop
  · nlinarith

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