integral_inv — Mathlib

English

If 0 is not contained in the closed interval [a,b], then the integral of 1/x over [a,b] equals log(b/a).

Русский

Если 0 не принадлежит замкнутому интервалу [a,b], то интеграл 1/x по [a,b] равен log(b/a).

LaTeX

$$$\forall a,b \in \mathbb{R},\ 0 \notin [a,b] \Rightarrow \displaystyle \int_a^b x^{-1} \, dx = \log\left( \frac{b}{a} \right)$$$

Lean4

@[simp]
theorem integral_inv (h : (0 : ℝ) ∉ [[a, b]]) : ∫ x in a..b, x⁻¹ = log (b / a) :=
  by
  have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
  rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
      (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
    log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]

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