integral_mul_deriv_eq_deriv_mul_of_integrable

English

If L is a bilinear map and the corresponding integrals converge, then the integral of L(u x, v' x) equals the negative of the integral of L(u' x, v x) plus boundary terms.

Русский

Пусть L билинейна; если интегралы сходятся, то интеграл L(u x, v' x) равен − интегралу L(u' x, v x) плюс границы.

LaTeX

$$$$ \int_{\mathbb{R}} L(u x, v' x) = -\int_{\mathbb{R}} L(u' x, v x) + (n - m). $$$$

Lean4

/-- **Integration by parts on (-∞, ∞).**
Version assuming that the total function is integrable -/
theorem integral_mul_deriv_eq_deriv_mul_of_integrable (hu : ∀ x, HasDerivAt u (u' x) x)
    (hv : ∀ x, HasDerivAt v (v' x) x) (huv' : Integrable (u * v')) (hu'v : Integrable (u' * v))
    (huv : Integrable (u * v)) : ∫ (x : ℝ), u x * v' x = -∫ (x : ℝ), u' x * v x :=
  integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable (L := ContinuousLinearMap.mul ℝ A) hu hv huv' hu'v huv

Похожие утверждения