English
The integral of the derivative of a product satisfies ∫ (u v') + (u' v) = u b v b − u a v a.
Русский
Интеграл производной произведения функций удовлетворяет формуле: ∫ (u v') + (u' v) = u(b) v(b) − u(a) v(a).
LaTeX
$$$\\int_{a}^{b} (u(x) v'(x) + u'(x) v(x))\,dx = u(b) v(b) - u(a) v(a)$$$
Lean4
theorem integral_eq_sub_of_hasDerivAt_of_tendsto (hab : a < b) {fa fb} (hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
(hint : IntervalIntegrable f' volume a b) (ha : Tendsto f (𝓝[>] a) (𝓝 fa)) (hb : Tendsto f (𝓝[<] b) (𝓝 fb)) :
∫ y in a..b, f' y = fb - fa := by
set F : ℝ → E := update (update f a fa) b fb
have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x :=
by
refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_
filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
unfold F
rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
have hcont : ContinuousOn F (Icc a b) :=
by
rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]
refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
· exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)
· rintro -
refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
simpa [F, hab.ne, hab.ne'] using integral_eq_sub_of_hasDerivAt_of_le hab.le hcont Fderiv hint
