integral_clm_comp_deriv_right_eq_neg_left

English

For Schwartz maps valued in continuous linear maps, the bilinear integration identity holds with deriv and evaluation in CLMs.

Русский

Для отображений Шварца, значения которых в непрерывно линейных отображениях, выполняется билинейная интеграционная формула с производной и оценкой в CLM.

LaTeX

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

Lean4

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

Version for a Schwartz function with values in continuous linear maps. -/
theorem integral_clm_comp_deriv_right_eq_neg_left (f : 𝓢(ℝ, F →L[𝕜] V)) (g : 𝓢(ℝ, F)) :
    ∫ (x : ℝ), f x (deriv g x) = -∫ (x : ℝ), deriv f x (g x) :=
  integral_bilinear_deriv_right_eq_neg_left f g ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] V)).bilinearRestrictScalars ℝ)

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