Derivatives of Schwartz functions #

In this file we define the various notions of derivatives of Schwartz functions.

Main definitions #

SchwartzMap.fderivCLM: The differential as a continuous linear map 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F)
SchwartzMap.derivCLM: The one-dimensional derivative as a continuous linear map 𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F)
SchwartzMap.instLineDeriv: The directional derivative with notation ∂_{m} f
SchwartzMap.instLaplacian: The Laplacian for 𝓢(E, F) as an instance of the notation type-class Laplacian.

Main statements #

SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv: the iterated directional derivative is given by the applied Fréchet derivative of a Schwartz function.
SchwartzMap.laplacian_eq_sum: the Laplacian is given by the sum of second derivatives in any orthonormal basis.
SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left: Integration by parts using the directional derivative ∂_{m}
SchwartzMap.integral_bilinear_laplacian_right_eq_left: Integration by parts for the Laplacian

Derivatives of Schwartz functions #

def SchwartzMap.derivCLM (𝕜 : Type u_2) (F : Type u_8) [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] :

SchwartzMap ℝ F →L[𝕜] SchwartzMap ℝ F

The 1-dimensional derivative on Schwartz space as a continuous 𝕜-linear map.

Equations

SchwartzMap.derivCLM 𝕜 F = SchwartzMap.mkCLM (fun (x : SchwartzMap ℝ F) => deriv ⇑x) ⋯ ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem SchwartzMap.derivCLM_apply (𝕜 : Type u_2) {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap ℝ F) (x : ℝ) :

((derivCLM 𝕜 F) f) x = deriv (⇑f) x

source

theorem SchwartzMap.hasDerivAt {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap ℝ F) (x : ℝ) :

HasDerivAt (⇑f) (deriv (⇑f) x) x

source

def SchwartzMap.fderivCLM (𝕜 : Type u_2) (E : Type u_5) (F : Type u_8) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] :

SchwartzMap E F →L[𝕜] SchwartzMap E (E →L[ℝ ] F)

The Fréchet derivative on Schwartz space as a continuous 𝕜-linear map.

Equations

SchwartzMap.fderivCLM 𝕜 E F = SchwartzMap.mkCLM (fun (x : SchwartzMap E F) => fderiv ℝ ⇑x) ⋯ ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem SchwartzMap.fderivCLM_apply (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E) :

((fderivCLM 𝕜 E F) f) x = fderiv ℝ (⇑f) x

source

theorem SchwartzMap.hasFDerivAt {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] (f : SchwartzMap E F) (x : E) :

HasFDerivAt (⇑f) (fderiv ℝ (⇑f) x) x

source

instance SchwartzMap.instLineDeriv {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] :

LineDeriv E (SchwartzMap E F) (SchwartzMap E F)

The partial derivative (or directional derivative) in the direction m : E as a continuous linear map on Schwartz space.

Equations

SchwartzMap.instLineDeriv = { lineDerivOp := fun (m : E) (f : SchwartzMap E F) => ((SchwartzMap.evalCLM ℝ E F m).comp (SchwartzMap.fderivCLM ℝ E F)) f }

source

theorem SchwartzMap.lineDerivOp_apply_eq_fderiv {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] (m : E) (f : SchwartzMap E F) (x : E) :

(LineDeriv.lineDerivOp m f) x = (fderiv ℝ (⇑f) x) m

source

instance SchwartzMap.instLineDerivAdd {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] :

LineDerivAdd E (SchwartzMap E F) (SchwartzMap E F)

source

instance SchwartzMap.instLineDerivSMul (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] :

LineDerivSMul 𝕜 E (SchwartzMap E F) (SchwartzMap E F)

source

instance SchwartzMap.instLineDerivLeftSMulReal {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] :

LineDerivLeftSMul ℝ E (SchwartzMap E F) (SchwartzMap E F)

source

instance SchwartzMap.instContinuousLineDeriv {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] :

ContinuousLineDeriv E (SchwartzMap E F) (SchwartzMap E F)

source

theorem SchwartzMap.lineDerivOpCLM_eq (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : E) :

LineDeriv.lineDerivOpCLM 𝕜 (SchwartzMap E F) m = (SchwartzMap.evalCLM 𝕜 E F m).comp (fderivCLM 𝕜 E F)

source

@[deprecated LineDeriv.lineDerivOpCLM (since := "2025-11-25")]

def SchwartzMap.pderivCLM (R : Type u_4) {V : Type u_5} (E : Type u_6) {F : Type u_7} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup V] [LineDeriv V E F] [LineDerivAdd V E F] [LineDerivSMul R V E F] [ContinuousLineDeriv V E F] (m : V) :

E →L[R] F

Alias of LineDeriv.lineDerivOpCLM.

Equations

SchwartzMap.pderivCLM = LineDeriv.lineDerivOpCLM

Instances For

source

@[deprecated LineDeriv.lineDerivOpCLM_apply (since := "2025-11-25")]

theorem SchwartzMap.pderivCLM_apply {R : Type u_4} {V : Type u_5} {E : Type u_6} {F : Type u_7} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup V] [LineDeriv V E F] [LineDerivAdd V E F] [LineDerivSMul R V E F] [ContinuousLineDeriv V E F] (m : V) (x : E) :

(LineDeriv.lineDerivOpCLM R E m) x = LineDeriv.lineDerivOp m x

Alias of LineDeriv.lineDerivOpCLM_apply.

source

theorem SchwartzMap.lineDerivOp_apply {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] (m : E) (f : SchwartzMap E F) (x : E) :

(LineDeriv.lineDerivOp m f) x = lineDeriv ℝ (⇑f) x m

source

theorem SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [NormedAddCommGroup D] [NormedSpace ℝ D] (m : D) (g : D ≃L[ℝ ] E) (f : SchwartzMap E F) :

LineDeriv.lineDerivOp m ((compCLMOfContinuousLinearEquiv 𝕜 g) f) = (compCLMOfContinuousLinearEquiv 𝕜 g) (LineDeriv.lineDerivOp (g m) f)

source

@[deprecated LineDeriv.iteratedLineDerivOpCLM (since := "2025-11-25")]

def SchwartzMap.iteratedPDeriv (R : Type u_4) {V : Type u_5} (E : Type u_6) [LineDeriv V E E] [TopologicalSpace E] [Ring R] [AddCommGroup V] [AddCommGroup E] [Module R E] [LineDerivAdd V E E] [LineDerivSMul R V E E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) :

E →L[R] E

Alias of LineDeriv.iteratedLineDerivOpCLM.

Equations

SchwartzMap.iteratedPDeriv = LineDeriv.iteratedLineDerivOpCLM

Instances For

source

@[deprecated LineDeriv.iteratedLineDerivOp_zero (since := "2025-11-25")]

theorem SchwartzMap.iteratedPDeriv_zero {V : Type u_14} {E : Type u_15} [LineDeriv V E E] (m : Fin 0 → V) (f : E) :

LineDeriv.iteratedLineDerivOp m f = f

Alias of LineDeriv.iteratedLineDerivOp_zero.

source

@[deprecated LineDeriv.iteratedLineDerivOp_one (since := "2025-11-25")]

theorem SchwartzMap.iteratedPDeriv_one {V : Type u_14} {E : Type u_15} [LineDeriv V E E] (m : Fin 1 → V) (f : E) :

LineDeriv.iteratedLineDerivOp m f = LineDeriv.lineDerivOp (m 0) f

Alias of LineDeriv.iteratedLineDerivOp_one.

source

@[deprecated LineDeriv.iteratedLineDerivOp_succ_left (since := "2025-11-25")]

theorem SchwartzMap.iteratedPDeriv_succ_left {V : Type u_14} {E : Type u_15} [LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E) :

LineDeriv.iteratedLineDerivOp m f = LineDeriv.lineDerivOp (m 0) (LineDeriv.iteratedLineDerivOp (Fin.tail m) f)

Alias of LineDeriv.iteratedLineDerivOp_succ_left.

source

@[deprecated LineDeriv.iteratedLineDerivOp_succ_right (since := "2025-11-25")]

theorem SchwartzMap.iteratedPDeriv_succ_right {V : Type u_14} {E : Type u_15} [LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E) :

LineDeriv.iteratedLineDerivOp m f = LineDeriv.iteratedLineDerivOp (Fin.init m) (LineDeriv.lineDerivOp (m (Fin.last n)) f)

Alias of LineDeriv.iteratedLineDerivOp_succ_right.

source

theorem SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] {n : ℕ} {m : Fin n → E} {f : SchwartzMap E F} {x : E} :

(LineDeriv.iteratedLineDerivOp m f) x = (iteratedFDeriv ℝ n (⇑f) x) m

source

@[deprecated SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv (since := "2025-11-25")]

theorem SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] {n : ℕ} {m : Fin n → E} {f : SchwartzMap E F} {x : E} :

(LineDeriv.iteratedLineDerivOp m f) x = (iteratedFDeriv ℝ n (⇑f) x) m

Alias of SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv.

Laplacian on `𝓢(E, F)` #

source

instance SchwartzMap.instLaplacian {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] :

Laplacian (SchwartzMap E F) (SchwartzMap E F)

Equations

SchwartzMap.instLaplacian = { laplacian := ⇑(LineDeriv.laplacianCLM ℝ E (SchwartzMap E F)) }

source

theorem SchwartzMap.laplacianCLM_eq' {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : SchwartzMap E F) :

(LineDeriv.laplacianCLM ℝ E (SchwartzMap E F)) f = Laplacian.laplacian f

source

theorem SchwartzMap.laplacian_eq_sum {ι : Type u_1} {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : SchwartzMap E F) :

Laplacian.laplacian f = ∑ i : ι, LineDeriv.lineDerivOp (b i) (LineDeriv.lineDerivOp (b i) f)

source

@[simp]

theorem SchwartzMap.laplacianCLM_eq (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap E F) :

(LineDeriv.laplacianCLM 𝕜 E (SchwartzMap E F)) f = Laplacian.laplacian f

source

theorem SchwartzMap.laplacian_apply {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : SchwartzMap E F) (x : E) :

(Laplacian.laplacian f) x = Laplacian.laplacian (⇑f) x

source

theorem SchwartzMap.integral_bilinear_deriv_right_eq_neg_left {E : Type u_5} {V : Type u_7} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [NormedAddCommGroup V] [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.

source

theorem SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul {𝕜 : Type u_2} [NormedRing 𝕜] [NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜] (f g : SchwartzMap ℝ 𝕜) :

∫ (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 multiplication of scalar-valued Schwartz functions.

source

theorem SchwartzMap.integral_smul_deriv_right_eq_neg_left {𝕜 : Type u_2} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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.

source

theorem SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left {𝕜 : Type u_2} {V : Type u_7} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] [NormedSpace ℝ V] [RCLike 𝕜] [NormedSpace 𝕜 F] [NormedSpace 𝕜 V] (f : SchwartzMap ℝ (F →L[𝕜] V)) (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.

source

theorem SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left {D : Type u_4} {E : Type u_5} {V : Type u_7} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup D] [NormedSpace ℝ D] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] (f : SchwartzMap D E) (g : SchwartzMap D F) (L : E →L[ℝ ] F →L[ℝ ] V) (v : D) :

∫ (x : D), (L (f x)) ((LineDeriv.lineDerivOp v g) x) ∂μ = -∫ (x : D), (L ((LineDeriv.lineDerivOp v f) x)) (g x) ∂μ

Integration by parts of Schwartz functions for directional derivatives.

Version for a general bilinear map.

source

theorem SchwartzMap.integral_mul_lineDerivOp_right_eq_neg_left {𝕜 : Type u_2} {D : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] [NormedRing 𝕜] [NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜] (f g : SchwartzMap D 𝕜) (v : D) :

∫ (x : D), f x * (LineDeriv.lineDerivOp v g) x ∂μ = -∫ (x : D), (LineDeriv.lineDerivOp v f) x * g x ∂μ

Integration by parts of Schwartz functions for directional derivatives.

Version for multiplication of scalar-valued Schwartz functions.

source

theorem SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left {𝕜 : Type u_2} {D : Type u_4} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup D] [NormedSpace ℝ D] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap D 𝕜) (g : SchwartzMap D F) (v : D) :

∫ (x : D), f x • (LineDeriv.lineDerivOp v g) x ∂μ = -∫ (x : D), (LineDeriv.lineDerivOp v f) x • g x ∂μ

Integration by parts of Schwartz functions for directional derivatives.

Version for scalar multiplication.

source

theorem SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left {𝕜 : Type u_2} {D : Type u_4} {V : Type u_7} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup D] [NormedSpace ℝ D] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] [RCLike 𝕜] [NormedSpace 𝕜 F] [NormedSpace 𝕜 V] (f : SchwartzMap D (F →L[𝕜] V)) (g : SchwartzMap D F) (v : D) :

∫ (x : D), (f x) ((LineDeriv.lineDerivOp v g) x) ∂μ = -∫ (x : D), ((LineDeriv.lineDerivOp v f) x) (g x) ∂μ

Integration by parts of Schwartz functions for directional derivatives.

Version for a Schwartz function with values in continuous linear maps.

Integration by parts #

source

theorem SchwartzMap.integral_bilinear_laplacian_right_eq_left {E : Type u_5} {F₁ : Type u_9} {F₂ : Type u_10} {F₃ : Type u_11} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) (L : F₁ →L[ℝ ] F₂ →L[ℝ ] F₃) :

∫ (x : E), (L (f x)) ((Laplacian.laplacian g) x) ∂μ = ∫ (x : E), (L ((Laplacian.laplacian f) x)) (g x) ∂μ

Integration by parts of Schwartz functions for the Laplacian.

Version for a general bilinear map.

source

theorem SchwartzMap.integral_mul_laplacian_right_eq_left {𝕜 : Type u_2} {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] [NormedRing 𝕜] [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.

source

theorem SchwartzMap.integral_smul_laplacian_right_eq_left {𝕜 : Type u_2} {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap E 𝕜) (g : SchwartzMap E F) :

∫ (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 scalar multiplication.

source

theorem SchwartzMap.integral_clm_comp_laplacian_right_eq_left {𝕜 : Type u_2} {E : Type u_5} {F₁ : Type u_9} {F₂ : Type u_10} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] [RCLike 𝕜] [NormedSpace 𝕜 F₁] [NormedSpace 𝕜 F₂] (f : SchwartzMap E (F₁ →L[𝕜] F₂)) (g : SchwartzMap E F₁) :

∫ (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 a Schwartz function with values in continuous linear maps.

Documentation

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Derivatives of Schwartz functions #

Main definitions #

Main statements #

Derivatives of Schwartz functions #

Laplacian on `𝓢(E, F)` #

Integration by parts #

Derivatives of Schwartz functions #

Main definitions #

Main statements #

Derivatives of Schwartz functions #

Laplacian on 𝓢(E, F) #

Integration by parts #

Laplacian on `𝓢(E, F)` #