integral_deriv_mul_eq_sub — Mathlib

English

If u and v have derivatives inside, the product-derivative identity holds with HasDerivAt from both ends.

Русский

Если у функций существует производная внутри и с обеих сторон, то формула для производной произведения справедлива.

LaTeX

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

Lean4

/-- Special case of `integral_deriv_mul_eq_sub_of_hasDeriv_right` where the functions have a
  derivative at the endpoints. -/
theorem integral_deriv_mul_eq_sub (hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x)
    (hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' volume a b)
    (hv' : IntervalIntegrable v' volume a b) : ∫ x in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a :=
  integral_deriv_mul_eq_sub_of_hasDerivWithinAt (fun x hx ↦ hu x hx |>.hasDerivWithinAt)
    (fun x hx ↦ hv x hx |>.hasDerivWithinAt) hu' hv'

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