English
In the integration by parts setting with bilinear L, the integral of L(u x, v' x) plus L(u' x, v x) equals n − m, where m,n arise from the limits of the bilinear term.
Русский
В рамках интегрирования по частям для билинейной формы L интеграл L(u x, v' x) + L(u' x, v x) dx равен n − m, где m,n — пределы билинейной части на бесконечности.
LaTeX
$$$$ \int_{\mathbb{R}} \bigl( L(u x, v' x) + L(u' x, v x) \bigr) \, dx = n - m, $$$$
Lean4
/-- **Integration by parts on (-∞, ∞).**
With respect to a general bilinear form. For the specific case of multiplication, see
`integral_mul_deriv_eq_deriv_mul`. -/
theorem integral_bilinear_hasDerivAt_right_eq_sub [CompleteSpace G] (hu : ∀ x, HasDerivAt u (u' x) x)
(hv : ∀ x, HasDerivAt v (v' x) x) (huv' : Integrable (fun x ↦ L (u x) (v' x)))
(hu'v : Integrable (fun x ↦ L (u' x) (v x))) (h_bot : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 m))
(h_top : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 n)) :
∫ (x : ℝ), L (u x) (v' x) = n - m - ∫ (x : ℝ), L (u' x) (v x) :=
by
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
exact integral_bilinear_hasDerivAt_eq_sub hu hv (huv'.add hu'v) h_bot h_top
