English
Let f, g be scalar- and vector-valued functions with derivatives as in the hypotheses, then ∫_a^b u(x) · v'(x) dx = u(b) · v(b) − u(a) · v(a) − ∫_a^b u'(x) · v(x) dx, in the vector-valued setting.
Русский
Пусть функции скаляра и вектора удовлетворяют предпосылкам, тогда ∫_a^b u(x) · v'(x) dx = u(b) · v(b) − u(a) · v(a) − ∫_a^b u'(x) · v(x) dx в векторном случае.
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
/-- **Integration by parts** (vector-valued). -/
theorem integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right (hu : ContinuousOn u [[a, b]])
(hv : ContinuousOn v [[a, b]]) (huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x)
(hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x) (hu' : IntervalIntegrable u' volume a b)
(hv' : IntervalIntegrable v' volume a b) :
∫ x in a..b, u x • v' x = u b • v b - u a • v a - ∫ x in a..b, u' x • v x :=
by
rw [← integral_deriv_smul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]
· simp_rw [add_sub_cancel_left]
· exact (hu'.smul_continuousOn hv).add (hv'.continuousOn_smul hu)
· exact hu'.smul_continuousOn hv
