English
For Schwartz maps f,g and a bilinear form L, the integral of L(f(x),g′(x)) equals the negative of the integral of L(f′(x),g(x)).
Русский
Для отображений Шварца f,g и билинейной формы L имеет место интеграл билинейной части: ∫ L(f(x), g′(x)) = - ∫ L(f′(x), g(x)).
LaTeX
$$$$ \\int f(x) (\\mathrm{deriv}\\, g(x)) \\, dx = - \\int (\\mathrm{deriv}\\, f(x)) g(x) \\, dx. $$$$
Lean4
/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.
Version for a general bilinear map. -/
theorem integral_bilinear_deriv_right_eq_neg_left (f : 𝓢(ℝ, E)) (g : 𝓢(ℝ, F)) (L : E →L[ℝ] F →L[ℝ] V) :
∫ (x : ℝ), L (f x) (deriv g x) = -∫ (x : ℝ), L (deriv f x) (g x) :=
MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable f.hasDerivAt g.hasDerivAt
(bilinLeftCLM L (derivCLM ℝ g).hasTemperateGrowth f).integrable
(bilinLeftCLM L g.hasTemperateGrowth (derivCLM ℝ f)).integrable (bilinLeftCLM L g.hasTemperateGrowth f).integrable
