integral_deriv_comp_smul_deriv — Mathlib

English

If HasDerivAt holds at the endpoints and interior has derivatives, the vector IBP identity holds between endpoints.

Русский

Если имеется HasDerivAt на концах и существующие внутри интервалы, формула IBP для вектора верна между концами.

LaTeX

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

Lean4

theorem integral_deriv_comp_smul_deriv (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, f' x • (g' ∘ f) x) = (g ∘ f) b - (g ∘ f) a :=
  integral_eq_sub_of_hasDerivAt (fun x hx ↦ (hg x hx).scomp x <| hf x hx)
    (hf'.smul (hg'.comp_continuousOn <| HasDerivAt.continuousOn hf)).intervalIntegrable

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