integral_deriv_comp_mul_deriv — Mathlib

English

The standard vector IBP equality: ∫_a^b (u x) v'(x) + u'(x) v(x) dx = u(b) v(b) − u(a) v(a).

Русский

Стандартное тождество IBP для векторных функций: ∫_a^b (u x) v'(x) + u'(x) v(x) dx = u(b) v(b) − u(a) v(a).

LaTeX

$$$\\displaystyle \\int_a^b (u(x) v'(x) + u'(x) v(x)) \\,dx = u(b) v(b) - u(a) v(a)$$$

Lean4

theorem integral_deriv_comp_mul_deriv {f f' g g' : ℝ → ℝ} (hf : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
    (hg : ∀ x ∈ uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (uIcc a b)) (hg' : Continuous g') :
    (∫ x in a..b, (g' ∘ f) x * f' x) = (g ∘ f) b - (g ∘ f) a := by
  simpa [mul_comm] using integral_deriv_comp_smul_deriv hf hg hf' hg'

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