Theorems · Theorem · functional analysis

SchwartzMap.integral_smul_deriv_right_eq_neg_left

∀ {𝕜 : Type u_2} {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 F] (f : SchwartzMap ℝ 𝕜) (g : SchwartzMap ℝ F),
  ∫ (x : ℝ), f x • deriv (⇑g) x = -∫ (x : ℝ), deriv (⇑f) x • g x

Integration by parts of Schwartz functions for the 1-dimensional derivative. Version for a Schwartz function with values in continuous linear maps.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceRCLikeNormedSpace