integral_mul_deriv_eq_neg_deriv_mul

English

Integration by parts for Schwartz maps with scalar-valued multiplication: ∫ f(x) (deriv g(x)) = -∫ (deriv f(x)) g(x).

Русский

Интегрирование по частям для отображений Шварца с умножением, т.е. ∫ f(x) deriv g(x) = -∫ deriv f(x) g(x).

LaTeX

$$$$ \\int f(x) \\cdot (\\mathrm{deriv}\\, g(x)) \\, dx = - \\int (\\mathrm{deriv}\\, f(x)) \\cdot g(x) \\, dx. $$$$

Lean4

/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.

Version for multiplication of scalar-valued Schwartz functions. -/
theorem integral_mul_deriv_eq_neg_deriv_mul (f : 𝓢(ℝ, 𝕜)) (g : 𝓢(ℝ, 𝕜)) :
    ∫ (x : ℝ), f x * (deriv g x) = -∫ (x : ℝ), deriv f x * (g x) :=
  integral_bilinear_deriv_right_eq_neg_left f g (ContinuousLinearMap.mul ℝ 𝕜)

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