intervalIntegrable_one_div_one_add_sq

English

Let μ be a locally finite measure on the real line. Then for every real a and b, the function x ↦ 1/(1 + x^2) is μ-integrable on the interval [a, b].

Русский

Пусть μ — локально конечная мера на ℝ. Тогда для любых a, b ∈ ℝ функция x ↦ 1/(1 + x^2) интегрируема по μ на отрезке [a, b].

LaTeX

$$$\forall a,b\in\mathbb{R},\ \int_{a}^{b} \frac{1}{1+x^{2}} \, d\mu < \infty$$$

Lean4

theorem intervalIntegrable_one_div_one_add_sq : IntervalIntegrable (fun x : ℝ => 1 / (↑1 + x ^ 2)) μ a b :=
  by
  refine (continuous_const.div ?_ fun x => ?_).intervalIntegrable a b
  · fun_prop
  · nlinarith

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