integral_deriv_mul_eq_sub — Mathlib

English

FTC-2 on (a, ∞): Under hypotheses about derivatives on Ioi a and integrability of the derivative, the improper integral over Ioi a equals the end difference b' - a'.

Русский

ТФК-2 на (a, ∞): при условии существования производной на Ioi a и интегрируемости производной, интеграл по Ioi a равен разности пределов.

LaTeX

$$$$ \int_{x \in Ioi a} u'(x) v(x) + u(x) v'(x) \, dx = b' - a', $$$$

Lean4

/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
theorem integral_deriv_mul_eq_sub [CompleteSpace A] (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
    (huv : Integrable (u' * v + u * v')) (h_bot : Tendsto (u * v) atBot (𝓝 a')) (h_top : Tendsto (u * v) atTop (𝓝 b')) :
    ∫ (x : ℝ), u' x * v x + u x * v' x = b' - a' :=
  integral_of_hasDerivAt_of_tendsto (fun x ↦ (hu x).mul (hv x)) huv h_bot h_top

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