English
Let A be a normed algebra over R and E a normed space, with u, u' : R → K (K = base field) and v, v' : R → E, differentiable on (a,b) with derivatives u' and v' respectively, and assume u', v' are interval-integrable on [a,b]. Then ∫_a^b u(x) · v'(x) + u'(x) · v(x) dx = u(b) · v(b) − u(a) · v(a).
Русский
Пусть A — нормированная алгебра над R, E — нормированное пространство, и функции u, u' : R → K, v, v' : R → E дифференцируемы на (a,b) с производными u', v' соответственно, а также у' и v' интегрируемы на интервале [a,b]. Тогда имеет место формула по частям для векторного умножения: ∫_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) \\cdot v'(x) \\,dx + \\int_a^b u'(x) \\cdot v(x) \\,dx = u(b) \\cdot v(b) - u(a) \\cdot v(a)$$$
Lean4
/-- The integral of the derivative of a scalar multiplication. -/
theorem integral_deriv_smul_eq_sub_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 x • v' x = u b • v b - u a • v a :=
by
simp_rw [add_comm]
apply integral_eq_sub_of_hasDeriv_right (hu.smul hv) fun x hx ↦ (huu' x hx).smul (hvv' x hx)
exact (hv'.continuousOn_smul hu).add (hu'.smul_continuousOn hv)
