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

noncomputable 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) ⋯ ⋯ ⋯ ⋯

@[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

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

noncomputable 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) ⋯ ⋯ ⋯ ⋯

@[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

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

@[instance_reducible]

noncomputable 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 ∘SL SchwartzMap.fderivCLM ℝ E F) f }

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

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)

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)

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)

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)

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 ∘SL fderivCLM 𝕜 E F

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

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

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] [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)

theorem SchwartzMap.tsupport_derivCLM_subset (𝕜 : Type u_2) {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap ℝ F) : tsupport ⇑((derivCLM 𝕜 F) f) ⊆ tsupport ⇑f

theorem SchwartzMap.tsupport_fderivCLM_subset (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) : tsupport ⇑((fderivCLM 𝕜 E F) f) ⊆ tsupport ⇑f

theorem SchwartzMap.tsupport_lineDerivOp_subset {E : Type u_5} {F : Type u_8} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] (m : E) (f : SchwartzMap E F) : tsupport ⇑(LineDeriv.lineDerivOp m f) ⊆ tsupport ⇑f

theorem SchwartzMap.tsupport_iteratedLineDerivOp_subset {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) : tsupport ⇑(LineDeriv.iteratedLineDerivOp m f) ⊆ tsupport ⇑f

Laplacian on 𝓢(E, F)

@[instance_reducible]

noncomputable 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)) }

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

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)

@[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

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

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.