Theorems · Theorem · functional analysis

SchwartzMap.integral_bilinear_deriv_right_eq_neg_left

∀ {E : Type u_5} {V : Type u_7} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedAddCommGroup V] [inst_5 : NormedSpace ℝ V]
  (f : SchwartzMap ℝ E) (g : SchwartzMap ℝ F) (L : E →L[ℝ] F →L[ℝ] V),
  ∫ (x : ℝ), (L (f x)) (deriv (⇑g) x) = -∫ (x : ℝ), (L (deriv (⇑f) x)) (g x)

Integration by parts of Schwartz functions for the 1-dimensional derivative. Version for a general bilinear map.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Cited by

3 results in Mathlib

Foundations

Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedAddCommGroupNormedSpace