English
Integration by parts for a bilinear form generalizes to equalities of integrals with derivatives on both sides of u and v.
Русский
Интегрирование по частям для билинейной формы обобщает равенства интегралов с производными слева и справа от u и v.
LaTeX
$$$$ \int (u x) (v' x) + \int (u' x) (v x) = \text{...}, $$$$
Lean4
/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`. -/
theorem integral_Ioi_deriv_mul_eq_sub (hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x)
(hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x) (huv : IntegrableOn (u' * v + u * v') (Ioi a))
(h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')) (h_infty : Tendsto (u * v) atTop (𝓝 b')) :
∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a' :=
by
rw [← Ici_diff_left] at h_zero
let f := Function.update (u * v) a a'
have hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x :=
by
intro x (hx : a < x)
apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy
exact Function.update_of_ne hy a' (u * v)
have htendsto : Tendsto f atTop (𝓝 b') := by
apply h_infty.congr'
filter_upwards [eventually_ne_atTop a] with x hx
exact (Function.update_of_ne hx a' (u * v)).symm
simpa using integral_Ioi_of_hasDerivAt_of_tendsto (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto
