English
Under a bilinear map L, with differentiable u and v and integrable bilinear terms, the integral of the bilinear combination equals the difference of the end values of the bilinear form.
Русский
При билинерной карте L и дифференцируемых u, v и интегрируемости соответствующих членов, интеграл билинейной комбинации равен разности концов.
LaTeX
$$$$ \int_{\mathbb{R}} L(u x, v' x) + L(u' x, v x) \, dx = n - m. $$$$
Lean4
/-- **Integration by parts on (-∞, ∞).**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
theorem integral_mul_deriv_eq_deriv_mul [CompleteSpace A] (hu : ∀ x, HasDerivAt u (u' x) x)
(hv : ∀ x, HasDerivAt v (v' x) x) (huv' : Integrable (u * v')) (hu'v : Integrable (u' * v))
(h_bot : Tendsto (u * v) atBot (𝓝 a')) (h_top : Tendsto (u * v) atTop (𝓝 b')) :
∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x :=
integral_bilinear_hasDerivAt_right_eq_sub (L := ContinuousLinearMap.mul ℝ A) hu hv huv' hu'v h_bot h_top
