feat(Analysis/Distribution): the Laplacian on Schwartz functions

Mathlib.lean

@@ -1784,6 +1784,7 @@ public import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
 public import Mathlib.Analysis.Distribution.DerivNotation
 public import Mathlib.Analysis.Distribution.Distribution
 public import Mathlib.Analysis.Distribution.FourierSchwartz
+public import Mathlib.Analysis.Distribution.Laplacian
 public import Mathlib.Analysis.Distribution.SchwartzSpace
 public import Mathlib.Analysis.Distribution.TemperateGrowth
 public import Mathlib.Analysis.Distribution.TemperedDistribution

Mathlib/Analysis/Distribution/DerivNotation.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Module.Equiv.Defs
 public import Mathlib.Data.Fin.Tuple.Basic
 public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Analysis.InnerProductSpace.CanonicalTensor
 
 /-! # Type classes for derivatives
 
@@ -21,11 +22,12 @@ test functions, distributions, tempered distributions, and Sobolev spaces (and o
 function spaces).
 -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 universe u' u v w
 
-variable {R V E F : Type*}
+variable {ι ι' 𝕜 R V E F F₁ F₂ F₃ V₁ V₂ V₃ : Type*}
+
 
 open Fin
 
@@ -93,13 +95,15 @@ end LineDeriv
 open LineDeriv
 
 /--
-The line derivative is additive, `∂_{v} (x + y) = ∂_{v} x + ∂_{v} y` for all `x y : E`.
+The line derivative is additive, `∂_{v} (x + y) = ∂_{v} x + ∂_{v} y` for all `x y : E`
+and `∂_{v + w} x = ∂_{v} x + ∂_{w} y` for all `v w : V`.
 
 Note that `lineDeriv` on functions is not additive.
 -/
 class LineDerivAdd (V : Type u) (E : Type v) (F : outParam (Type w))
-    [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] where
+    [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] where
   lineDerivOp_add (v : V) (x y : E) : ∂_{v} (x + y) = ∂_{v} x + ∂_{v} y
+  lineDerivOp_left_add (v w : V) (x : E) : ∂_{v + w} x = ∂_{v} x + ∂_{w} x
 
 /--
 The line derivative commutes with scalar multiplication, `∂_{v} (r • x) = r • ∂_{v} x` for all
@@ -109,6 +113,14 @@ class LineDerivSMul (R : Type*) (V : Type u) (E : Type v) (F : outParam (Type w)
     [SMul R E] [SMul R F] [LineDeriv V E F] where
   lineDerivOp_smul (v : V) (r : R) (x : E) : ∂_{v} (r • x) = r • ∂_{v} x
 
+/--
+The line derivative commutes with scalar multiplication, `∂_{r • v} x = r • ∂_{v} x` for all
+`r : R` and `v : V`.
+-/
+class LineDerivLeftSMul (R : Type*) (V : Type u) (E : Type v) (F : outParam (Type w))
+    [SMul R V] [SMul R F] [LineDeriv V E F] where
+  lineDerivOp_left_smul (r : R) (v : V) (x : E) : ∂_{r • v} x = r • ∂_{v} x
+
 /--
 The line derivative is continuous.
 -/
@@ -121,13 +133,15 @@ attribute [fun_prop] ContinuousLineDeriv.continuous_lineDerivOp
 namespace LineDeriv
 
 export LineDerivAdd (lineDerivOp_add)
+export LineDerivAdd (lineDerivOp_left_add)
 export LineDerivSMul (lineDerivOp_smul)
+export LineDerivLeftSMul (lineDerivOp_left_smul)
 export ContinuousLineDeriv (continuous_lineDerivOp)
 
 section lineDerivOpCLM
 
 variable [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F]
-  [TopologicalSpace E] [TopologicalSpace F]
+  [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup V]
   [LineDeriv V E F] [LineDerivAdd V E F] [LineDerivSMul R V E F] [ContinuousLineDeriv V E F]
 
 variable (R E) in
@@ -149,7 +163,7 @@ section iteratedLineDerivOp
 variable [LineDeriv V E E]
 variable {n : ℕ} (m : Fin n → V)
 
-theorem iteratedLineDerivOp_add [AddCommGroup E] [LineDerivAdd V E E] (x y : E) :
+theorem iteratedLineDerivOp_add [AddCommGroup V] [AddCommGroup E] [LineDerivAdd V E E] (x y : E) :
     ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y := by
   induction n with
   | zero =>
@@ -176,7 +190,7 @@ theorem continuous_iteratedLineDerivOp [ContinuousLineDeriv V E E] {n : ℕ} (m
   | succ n IH =>
     exact (continuous_lineDerivOp _).comp (IH _)
 
-variable [Ring R] [AddCommGroup E] [Module R E]
+variable [Ring R] [AddCommGroup V] [AddCommGroup E] [Module R E]
   [LineDerivAdd V E E] [LineDerivSMul R V E E] [ContinuousLineDeriv V E E]
 
 variable (R E) in
@@ -194,3 +208,108 @@ theorem iteratedLineDerivOpCLM_apply {n : ℕ} (m : Fin n → V) (x : E) :
 end iteratedLineDerivOp
 
 end LineDeriv
+
+/--
+The notation typeclass for the Laplace operator.
+-/
+class Laplacian (E : Type v) (F : outParam (Type w)) where
+  /-- `Δ f` is the Laplacian of `f`. The meaning of this notation is type-dependent. -/
+  laplacian : E → F
+
+namespace Laplacian
+
+@[inherit_doc] scoped notation "Δ" => Laplacian.laplacian
+
+end Laplacian
+
+namespace LineDeriv
+
+variable [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃]
+  [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃]
+
+/-! ## Laplacian of `LineDeriv` -/
+
+section TensorProduct
+
+variable [CommRing R] [AddCommGroup E] [Module R E]
+  [Module R V₂] [Module R V₃]
+  [LineDerivAdd E V₂ V₃] [LineDerivAdd E V₁ V₂]
+  [LineDerivSMul R E V₂ V₃] [LineDerivLeftSMul R E V₁ V₂] [LineDerivLeftSMul R E V₂ V₃]
+
+open InnerProductSpace TensorProduct
+
+variable (R) in
+/-- The second derivative as a bilinear map.
+
+Mainly used to give an abstract definition of the Laplacian. -/
+def bilinearLineDerivTwo (f : V₁) : E →ₗ[R] E →ₗ[R] V₃ :=
+  LinearMap.mk₂ R (∂_{·} <| ∂_{·} f) (by simp [lineDerivOp_left_add])
+    (by simp [lineDerivOp_left_smul]) (by simp [lineDerivOp_left_add, lineDerivOp_add])
+    (by simp [lineDerivOp_left_smul, lineDerivOp_smul])
+
+variable (R) in
+/-- The second derivative as a linear map from the tensor product.
+
+Mainly used to give an abstract definition of the Laplacian. -/
+def tensorLineDerivTwo (f : V₁) : E ⊗[R] E →ₗ[R] V₃ :=
+  lift (bilinearLineDerivTwo R f)
+
+lemma tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp (f : V₁) (v w : E) :
+    tensorLineDerivTwo R f (v ⊗ₜ[R] w) = ∂_{v} (∂_{w} f) := lift.tmul _ _
+
+end TensorProduct
+
+section InnerProductSpace
+
+variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+
+section LinearMap
+
+variable [CommRing R]
+  [Module R E] [Module ℝ V₂] [Module ℝ V₃]
+  [LineDerivAdd E V₁ V₂] [LineDerivAdd E V₂ V₃]
+  [LineDerivSMul ℝ E V₂ V₃] [LineDerivLeftSMul ℝ E V₁ V₂] [LineDerivLeftSMul ℝ E V₂ V₃]
+
+open TensorProduct InnerProductSpace
+
+theorem tensorLineDerivTwo_canonicalCovariantTensor_eq_sum [Fintype ι] (v : OrthonormalBasis ι ℝ E)
+    (f : V₁) : tensorLineDerivTwo ℝ f (canonicalCovariantTensor E) = ∑ i, ∂_{v i} (∂_{v i} f) := by
+  simp [InnerProductSpace.canonicalCovariantTensor_eq_sum E v,
+    tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp]
+
+end LinearMap
+
+section ContinuousLinearMap
+
+section definition
+
+variable [CommRing R]
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  [Module R V₁] [Module R V₂] [Module R V₃]
+  [TopologicalSpace V₁] [TopologicalSpace V₂] [TopologicalSpace V₃] [IsTopologicalAddGroup V₃]
+  [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₁ V₂] [ContinuousLineDeriv E V₁ V₂]
+  [LineDerivAdd E V₂ V₃] [LineDerivSMul R E V₂ V₃] [ContinuousLineDeriv E V₂ V₃]
+
+variable (R E V₁) in
+/-- The Laplacian defined by iterated `lineDerivOp` as a continuous linear map. -/
+def laplacianCLM : V₁ →L[R] V₃ :=
+  ∑ i, lineDerivOpCLM R V₂ (stdOrthonormalBasis ℝ E i) ∘L
+    lineDerivOpCLM R V₁ (stdOrthonormalBasis ℝ E i)
+
+end definition
+
+variable [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₃]
+  [TopologicalSpace V₁] [TopologicalSpace V₂] [TopologicalSpace V₃] [IsTopologicalAddGroup V₃]
+  [LineDerivAdd E V₁ V₂] [LineDerivSMul ℝ E V₁ V₂] [ContinuousLineDeriv E V₁ V₂]
+  [LineDerivAdd E V₂ V₃] [LineDerivSMul ℝ E V₂ V₃] [ContinuousLineDeriv E V₂ V₃]
+  [LineDerivLeftSMul ℝ E V₁ V₂] [LineDerivLeftSMul ℝ E V₂ V₃]
+
+theorem laplacianCLM_eq_sum [Fintype ι] (v : OrthonormalBasis ι ℝ E) (f : V₁) :
+    laplacianCLM ℝ E V₁ f = ∑ i, ∂_{v i} (∂_{v i} f) := by
+  simp [laplacianCLM, ← tensorLineDerivTwo_canonicalCovariantTensor_eq_sum]
+
+end ContinuousLinearMap
+
+end InnerProductSpace
+
+end LineDeriv

Mathlib/Analysis/Distribution/Laplacian.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2025 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+module
+
+public import Mathlib.Analysis.Distribution.TemperedDistribution
+public import Mathlib.Analysis.InnerProductSpace.Laplacian
+
+/-! # The Laplacian on Schwartz functions
+
+We define the Laplacian on Schwartz functions.
+
+## Main definitions
+
+* `LineDeriv.laplacianCLM`: The abstract definition of a Laplacian as a sum over the second
+  derivatives.
+* `SchwartzMap.instLaplacian`: The Laplacian for `𝓢(E, F)` as an instance of the notation type-class
+  `Laplacian`.
+
+## Main statements
+* `SchwartzMap.laplacian_eq_sum`: The Laplacian is equal to the sum of second derivatives in any
+  orthonormal basis.
+* `SchwartzMap.integral_bilinear_laplacian_right_eq_left`: Integration by parts for the Laplacian.
+
+## Implementation notes
+The abstract definition `LineDeriv.laplacianCLM` does not provide an instance of `Laplacian` because
+the type-class system is not able to infer the inner product space `E`. In order to avoid duplicated
+definitions, we do not define `LineDeriv.laplacian` and subsequently every concrete instance of
+`LineDeriv` has to provide an instance for `Laplacian` and a proof that
+`LineDeriv.laplacianCLM _ _ _ f = Δ f`, for example see `SchwartzMap.laplacianCLM_eq'` and
+`SchwartzMap.laplacian_eq_sum'` below.
+
+We also note that since `LineDeriv` merely notation and not tied to `fderiv`, it is not possible to
+prove the independence of the basis in the definition of the Laplacian in the abstract setting.
+In the case of sufficiently smooth functions, this follows from an equality of `lineDerivOp` and
+`fderiv`, see for example `SchwartzMap.coe_laplacian_eq_sum`, and in the case of distributions, this
+follows from duality. Therefore, when implementing `Laplacian` using `LineDeriv.laplacianCLM`, you
+should prove a version of `SchwartzMap.laplacian_eq_sum`.
+
+-/
+
+@[expose] public noncomputable section
+
+variable {ι ι' 𝕜 R E F F₁ F₂ F₃ V₁ V₂ V₃ : Type*}
+
+variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  [NormedAddCommGroup F]
+
+namespace SchwartzMap
+
+/-! ## Laplacian on `𝓢(E, F)` -/
+
+variable [NormedSpace ℝ F]
+
+open Laplacian LineDeriv
+
+instance instLaplacian : Laplacian 𝓢(E, F) 𝓢(E, F) where
+  laplacian := laplacianCLM ℝ E 𝓢(E, F)
+
+theorem laplacianCLM_eq' (f : 𝓢(E, F)) : laplacianCLM ℝ E 𝓢(E, F) f = Δ f := rfl
+
+theorem laplacian_eq_sum [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : 𝓢(E, F)) :
+    Δ f = ∑ i, ∂_{b i} (∂_{b i} f) :=
+  LineDeriv.laplacianCLM_eq_sum b f
+
+variable (𝕜) in
+@[simp]
+theorem laplacianCLM_eq [RCLike 𝕜] [NormedSpace 𝕜 F] (f : 𝓢(E, F)) :
+    laplacianCLM 𝕜 E 𝓢(E, F) f = Δ f := by
+  simp [laplacianCLM, laplacian_eq_sum (stdOrthonormalBasis ℝ E)]
+
+theorem laplacian_apply (f : 𝓢(E, F)) (x : E) : Δ f x = Δ (f : E → F) x := by
+  rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E)]
+  simp only [InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f
+    (stdOrthonormalBasis ℝ E), sum_apply]
+  congr 1
+  ext i
+  rw [← iteratedLineDerivOp_eq_iteratedFDeriv]
+  rfl
+
+open MeasureTheory
+
+/-! ### Integration by parts -/
+
+variable
+  [NormedAddCommGroup F₁] [NormedSpace ℝ F₁]
+  [NormedAddCommGroup F₂] [NormedSpace ℝ F₂]
+  [NormedAddCommGroup F₃] [NormedSpace ℝ F₃]
+  [MeasurableSpace E] {μ : Measure E} [BorelSpace E] [μ.IsAddHaarMeasure]
+
+/-- Integration by parts of Schwartz functions for the Laplacian.
+
+Version for a general bilinear map. -/
+theorem integral_bilinear_laplacian_right_eq_left (f : 𝓢(E, F₁)) (g : 𝓢(E, F₂))
+    (L : F₁ →L[ℝ] F₂ →L[ℝ] F₃) :
+    ∫ x, L (f x) (Δ g x) ∂μ = ∫ x, L (Δ f x) (g x) ∂μ := by
+  simp_rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E), sum_apply, map_sum,
+    ContinuousLinearMap.coe_sum', Finset.sum_apply]
+  rw [MeasureTheory.integral_finset_sum, MeasureTheory.integral_finset_sum]
+  · simp [integral_bilinear_lineDerivOp_right_eq_neg_left]
+  · exact fun _ _ ↦ (pairing L (∂_{_} <| ∂_{_} f) g).integrable
+  · exact fun _ _ ↦ (pairing L f (∂_{_} <| ∂_{_} g)).integrable
+
+variable [NormedRing 𝕜] [NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜] in
+/-- Integration by parts of Schwartz functions for the Laplacian.
+
+Version for multiplication of scalar-valued Schwartz functions. -/
+theorem integral_mul_laplacian_right_eq_left (f : 𝓢(E, 𝕜)) (g : 𝓢(E, 𝕜)) :
+    ∫ x, f x * Δ g x ∂μ = ∫ x, Δ f x * g x ∂μ :=
+  integral_bilinear_laplacian_right_eq_left f g (ContinuousLinearMap.mul ℝ 𝕜)
+
+variable [RCLike 𝕜] [NormedSpace 𝕜 F]
+
+/-- Integration by parts of Schwartz functions for the Laplacian.
+
+Version for scalar multiplication. -/
+theorem integral_smul_laplacian_right_eq_left (f : 𝓢(E, 𝕜)) (g : 𝓢(E, F)) :
+    ∫ x, f x • Δ g x ∂μ = ∫ x, Δ f x • g x ∂μ :=
+  integral_bilinear_laplacian_right_eq_left f g (ContinuousLinearMap.lsmul ℝ 𝕜)
+
+variable [NormedSpace 𝕜 F₁] [NormedSpace 𝕜 F₂]
+
+/-- Integration by parts of Schwartz functions for the Laplacian.
+
+Version for a Schwartz function with values in continuous linear maps. -/
+theorem integral_clm_comp_laplacian_right_eq_left (f : 𝓢(E, F₁ →L[𝕜] F₂)) (g : 𝓢(E, F₁)) :
+    ∫ x, f x (Δ g x) ∂μ = ∫ x, Δ f x (g x) ∂μ :=
+  integral_bilinear_laplacian_right_eq_left f g
+    ((ContinuousLinearMap.id 𝕜 (F₁ →L[𝕜] F₂)).bilinearRestrictScalars ℝ)
+
+end SchwartzMap

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -1033,17 +1033,29 @@ continuous linear map on Schwartz space. -/
 instance instLineDeriv : LineDeriv E 𝓢(E, F) 𝓢(E, F) where
   lineDerivOp m f := (SchwartzMap.evalCLM m).comp (fderivCLM ℝ E F) f
 
+theorem lineDerivOp_apply (m : E) (f : 𝓢(E, F)) (x : E) : ∂_{m} f x = lineDeriv ℝ f x m :=
+  f.differentiableAt.lineDeriv_eq_fderiv.symm
+
+theorem lineDerivOp_apply_eq_fderiv (m : E) (f : 𝓢(E, F)) (x : E) :
+    ∂_{m} f x = fderiv ℝ f x m := rfl
+
 instance instLineDerivAdd : LineDerivAdd E 𝓢(E, F) 𝓢(E, F) where
   lineDerivOp_add m := ((SchwartzMap.evalCLM m).comp (fderivCLM ℝ E F)).map_add
+  lineDerivOp_left_add v w f := by
+    ext x
+    simp [lineDerivOp_apply_eq_fderiv]
 
 instance instLineDerivSMul : LineDerivSMul 𝕜 E 𝓢(E, F) 𝓢(E, F) where
   lineDerivOp_smul m := ((SchwartzMap.evalCLM m).comp (fderivCLM 𝕜 E F)).map_smul
 
+instance instLineDerivLeftSMul : LineDerivLeftSMul ℝ E 𝓢(E, F) 𝓢(E, F) where
+  lineDerivOp_left_smul r y f := by
+    ext x
+    simp [lineDerivOp_apply_eq_fderiv]
+
 instance instContinuousLineDeriv : ContinuousLineDeriv E 𝓢(E, F) 𝓢(E, F) where
   continuous_lineDerivOp m := ((SchwartzMap.evalCLM m).comp (fderivCLM ℝ E F)).continuous
 
-open LineDeriv
-
 theorem lineDerivOpCLM_eq (m : E) :
     lineDerivOpCLM 𝕜 𝓢(E, F) m = (SchwartzMap.evalCLM m).comp (fderivCLM 𝕜 E F) := rfl
 
@@ -1053,12 +1065,6 @@ alias pderivCLM := lineDerivOpCLM
 @[deprecated (since := "2025-11-25")]
 alias pderivCLM_apply := LineDeriv.lineDerivOpCLM_apply
 
-theorem lineDerivOp_apply (m : E) (f : 𝓢(E, F)) (x : E) : ∂_{m} f x = lineDeriv ℝ f x m :=
-  f.differentiableAt.lineDeriv_eq_fderiv.symm
-
-theorem lineDerivOp_apply_eq_fderiv (m : E) (f : 𝓢(E, F)) (x : E) :
-    ∂_{m} f x = fderiv ℝ f x m := rfl
-
 @[deprecated (since := "2025-11-25")]
 alias iteratedPDeriv := LineDeriv.iteratedLineDerivOpCLM
 
@@ -1490,5 +1496,6 @@ theorem integral_clm_comp_lineDerivOp_right_eq_neg_left (f : 𝓢(D, F →L[𝕜
 
 end integration_by_parts
 
-
 end SchwartzMap
+
+set_option linter.style.longFile 1700