intervalIntegrable_inv_one_add_sq

English

Let μ be a locally finite measure on ℝ. Then for every a,b ∈ ℝ, the function x ↦ (1 + x^2)⁻¹ is μ-integrable on [a,b].

Русский

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

LaTeX

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

Lean4

@[simp]
theorem intervalIntegrable_inv_one_add_sq : IntervalIntegrable (fun x : ℝ => (↑1 + x ^ 2)⁻¹) μ a b := by
  simp [← one_div, intervalIntegrable_one_div_one_add_sq]

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