Theorems · Theorem · functional analysis

SchwartzMap.integral_mul_laplacian_right_eq_left

∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E]
  [μ.IsAddHaarMeasure] [inst_6 : NormedRing 𝕜] [inst_7 : NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜]
  (f g : SchwartzMap E 𝕜), ∫ (x : E), f x * (Laplacian.laplacian g) x ∂μ = ∫ (x : E), (Laplacian.laplacian f) x * g x ∂μ

Integration by parts of Schwartz functions for the Laplacian. Version for multiplication of scalar-valued Schwartz functions.

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasureNormedRingNormedSpaceIsScalarTowerSMulCommClass