diff --git a/Mathlib/Analysis/Distribution/DerivNotation.lean b/Mathlib/Analysis/Distribution/DerivNotation.lean
index e5344004c3a6e0..46370ad6787890 100644
--- a/Mathlib/Analysis/Distribution/DerivNotation.lean
+++ b/Mathlib/Analysis/Distribution/DerivNotation.lean
@@ -194,3 +194,16 @@ 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
diff --git a/Mathlib/Analysis/Distribution/FourierMultiplier.lean b/Mathlib/Analysis/Distribution/FourierMultiplier.lean
new file mode 100644
index 00000000000000..c592d0d3b07f43
--- /dev/null
+++ b/Mathlib/Analysis/Distribution/FourierMultiplier.lean
@@ -0,0 +1,203 @@
+/-
+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.Laplacian
+
+/-! # Fourier multiplier on Schwartz functions and tempered distributions -/
+
+@[expose] public noncomputable section
+
+variable {ι 𝕜 E F F₁ F₂ : Type*}
+
+namespace SchwartzMap
+
+open scoped SchwartzMap
+
+variable [RCLike 𝕜]
+  [NormedAddCommGroup E] [NormedAddCommGroup F]
+  [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F]
+  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+
+open FourierTransform
+
+variable (F) in
+def fourierMultiplierCLM (g : E → 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F) :=
+  fourierInvCLM 𝕜 𝓢(E, F) ∘L (smulLeftCLM F g) ∘L fourierCLM 𝕜 𝓢(E, F)
+
+theorem fourierMultiplierCLM_apply (g : E → 𝕜) (f : 𝓢(E, F)) :
+    fourierMultiplierCLM F g f = 𝓕⁻ (smulLeftCLM F g (𝓕 f)) := by
+  rfl
+
+variable (𝕜) in
+theorem fourierMultiplierCLM_ofReal {g : E → ℝ} (hg : g.HasTemperateGrowth) (f : 𝓢(E, F)) :
+    fourierMultiplierCLM F (fun x ↦ RCLike.ofReal (K := 𝕜) (g x)) f =
+    fourierMultiplierCLM F g f := by
+  simp_rw [fourierMultiplierCLM_apply]
+  congr 1
+  exact smulLeftCLM_ofReal 𝕜 hg (𝓕 f)
+
+theorem fourierMultiplierCLM_smul_apply {g : E → 𝕜} (hg : g.HasTemperateGrowth) (c : 𝕜)
+    (f : 𝓢(E, F)) :
+    fourierMultiplierCLM F (c • g) f = c • fourierMultiplierCLM F g f := by
+  simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]
+
+theorem fourierMultiplierCLM_smul {g : E → 𝕜} (hg : g.HasTemperateGrowth) (c : 𝕜) :
+    fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g := by
+  ext1 f
+  exact fourierMultiplierCLM_smul_apply hg c f
+
+variable (F) in
+theorem fourierMultiplierCLM_sum {g : ι → E → 𝕜} {s : Finset ι}
+    (hg : ∀ i ∈ s, (g i).HasTemperateGrowth) :
+    fourierMultiplierCLM F (fun x ↦ ∑ i ∈ s, g i x) = ∑ i ∈ s, fourierMultiplierCLM F (g i) := by
+  ext1 f
+  simpa [fourierMultiplierCLM_apply, smulLeftCLM_sum hg] using map_sum _ _ _
+
+variable [CompleteSpace F]
+
+@[simp]
+theorem fourierMultiplierCLM_const (c : 𝕜) :
+    fourierMultiplierCLM F (fun (_ : E) ↦ c) = c • ContinuousLinearMap.id _ _ := by
+  ext f x
+  simp [fourierMultiplierCLM_apply]
+
+theorem fourierMultiplierCLM_fourierMultiplierCLM_apply {g₁ g₂ : E → 𝕜}
+    (hg₁ : g₁.HasTemperateGrowth) (hg₂ : g₂.HasTemperateGrowth) (f : 𝓢(E, F)) :
+    fourierMultiplierCLM F g₁ (fourierMultiplierCLM F g₂ f) =
+    fourierMultiplierCLM F (g₁ * g₂) f := by
+  simp [fourierMultiplierCLM_apply, smulLeftCLM_smulLeftCLM_apply hg₁ hg₂]
+
+open LineDeriv Laplacian Real
+
+theorem lineDeriv_eq_fourierMultiplierCLM (m : E) (f : 𝓢(E, F)) :
+    ∂_{m} f = (2 * π * Complex.I) • fourierMultiplierCLM F (inner ℝ · m) f := by
+  rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
+    FourierTransform.fourierInv_fourier_eq]
+
+theorem laplacian_eq_fourierMultiplierCLM (f : 𝓢(E, F)) :
+    Δ f = -(2 * π) ^ 2 • fourierMultiplierCLM F (‖·‖ ^ 2) f := by
+  let ι := Fin (Module.finrank ℝ E)
+  let b := stdOrthonormalBasis ℝ E
+  have : ∀ i (hi : i ∈ Finset.univ), (inner ℝ · (b i) ^ 2).HasTemperateGrowth := by
+    fun_prop
+  simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, fourierMultiplierCLM_sum F this,
+    ContinuousLinearMap.coe_sum', Finset.sum_apply, Finset.smul_sum]
+  congr 1
+  ext i x
+  simp_rw [smul_apply, lineDeriv_eq_fourierMultiplierCLM]
+  rw [← fourierMultiplierCLM_ofReal ℂ (by fun_prop)]
+  simp_rw [map_smul, smul_apply, smul_smul]
+  congr 1
+  · ring_nf
+    simp
+  rw [fourierMultiplierCLM_ofReal ℂ (by fun_prop)]
+  rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
+  congr 3
+  ext y
+  simp [pow_two]
+
+end SchwartzMap
+
+namespace TemperedDistribution
+
+open scoped SchwartzMap
+
+variable [NormedAddCommGroup E] [NormedAddCommGroup F]
+  [InnerProductSpace ℝ E] [NormedSpace ℂ F]
+  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+
+open FourierTransform
+
+variable (F) in
+def fourierMultiplierCLM (g : E → ℂ) : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
+  fourierInvCLM ℂ 𝓢'(E, F) ∘L (smulLeftCLM F g) ∘L fourierCLM ℂ 𝓢'(E, F)
+
+theorem fourierMultiplierCLM_apply (g : E → ℂ) (f : 𝓢'(E, F)) :
+    fourierMultiplierCLM F g f = 𝓕⁻ (smulLeftCLM F g (𝓕 f)) := by
+  rfl
+
+@[simp]
+theorem fourierMultiplierCLM_apply_apply (g : E → ℂ) (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)) :
+    fourierMultiplierCLM F g f u = f (𝓕 (SchwartzMap.smulLeftCLM ℂ g (𝓕⁻ u))) := by
+  rfl
+
+@[simp]
+theorem fourierMultiplierCLM_const_apply (f : 𝓢'(E, F)) (c : ℂ) :
+    fourierMultiplierCLM F (fun _ ↦ c) f = c • f := by
+  ext
+  simp
+
+theorem fourierMultiplierCLM_fourierMultiplierCLM_apply {g₁ g₂ : E → ℂ}
+    (hg₁ : g₁.HasTemperateGrowth) (hg₂ : g₂.HasTemperateGrowth) (f : 𝓢'(E, F)) :
+    fourierMultiplierCLM F g₂ (fourierMultiplierCLM F g₁ f) =
+    fourierMultiplierCLM F (g₁ * g₂) f := by
+  simp [fourierMultiplierCLM_apply, smulLeftCLM_smulLeftCLM_apply hg₁ hg₂]
+
+theorem fourierMultiplierCLM_smul_apply {g : E → ℂ} (hg : g.HasTemperateGrowth) (c : ℂ)
+    (f : 𝓢'(E, F)) :
+    fourierMultiplierCLM F (c • g) f = c • fourierMultiplierCLM F g f := by
+  simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]
+
+theorem fourierMultiplierCLM_smul {g : E → ℂ} (hg : g.HasTemperateGrowth) (c : ℂ) :
+    fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g := by
+  ext1 f
+  exact fourierMultiplierCLM_smul_apply hg c f
+
+section embedding
+
+variable [CompleteSpace F]
+
+theorem fourierMultiplierCLM_toTemperedDistributionCLM_eq {g : E → ℂ}
+    (hg : g.HasTemperateGrowth) (f : 𝓢(E, F)) :
+    fourierMultiplierCLM F g (f : 𝓢'(E, F)) = SchwartzMap.fourierMultiplierCLM F g f := by
+  ext u
+  simp [SchwartzMap.integral_fourier_smul_eq, SchwartzMap.fourierMultiplierCLM_apply g f,
+    ← SchwartzMap.integral_fourierInv_smul_eq, hg, smul_smul, mul_comm]
+
+end embedding
+
+variable (F) in
+theorem fourierMultiplierCLM_sum {g : ι → E → ℂ} {s : Finset ι}
+    (hg : ∀ i ∈ s, (g i).HasTemperateGrowth) :
+    fourierMultiplierCLM F (fun x ↦ ∑ i ∈ s, g i x) = ∑ i ∈ s, fourierMultiplierCLM F (g i) := by
+  ext f u
+  have : 𝓕 (∑ x ∈ s, (SchwartzMap.smulLeftCLM ℂ (g x)) (𝓕⁻ u)) =
+      ∑ x ∈ s, 𝓕 ((SchwartzMap.smulLeftCLM ℂ (g x)) (𝓕⁻ u)) :=
+    map_sum (fourierCLM ℂ 𝓢(E, ℂ)) (fun i ↦ SchwartzMap.smulLeftCLM ℂ (g i) (𝓕⁻ u)) s
+  simp [SchwartzMap.smulLeftCLM_sum hg, UniformConvergenceCLM.sum_apply, this]
+
+open LineDeriv Laplacian Real
+
+theorem lineDeriv_eq_fourierMultiplierCLM (m : E) (f : 𝓢'(E, F)) :
+    ∂_{m} f = (2 * π * Complex.I) • fourierMultiplierCLM F (inner ℝ · m) f := by
+  rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
+    FourierTransform.fourierInv_fourier_eq]
+
+theorem laplacian_eq_fourierMultiplierCLM (f : 𝓢'(E, F)) :
+    Δ f = -(2 * π) ^ 2 • fourierMultiplierCLM F (fun x ↦ Complex.ofReal (‖x‖ ^ 2)) f := by
+  let ι := Fin (Module.finrank ℝ E)
+  let b := stdOrthonormalBasis ℝ E
+  have : ∀ i (hi : i ∈ Finset.univ),
+      (fun x ↦ Complex.ofReal (inner ℝ x (b i)) ^ 2).HasTemperateGrowth := by
+    fun_prop
+  simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, Complex.ofReal_sum, Complex.ofReal_pow,
+    fourierMultiplierCLM_sum F this,
+    ContinuousLinearMap.coe_sum', Finset.sum_apply, Finset.smul_sum]
+  congr 1
+  ext i x
+  simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]
+  rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
+  rw [← Complex.coe_smul (-(2 * π) ^ 2)]
+  congr 4
+  · ring_nf
+    simp
+  · ext y
+    simp
+    ring
+
+
+end TemperedDistribution
diff --git a/Mathlib/Analysis/Distribution/FourierSchwartz.lean b/Mathlib/Analysis/Distribution/FourierSchwartz.lean
index 98db5e4ac2d534..ed766748c77af1 100644
--- a/Mathlib/Analysis/Distribution/FourierSchwartz.lean
+++ b/Mathlib/Analysis/Distribution/FourierSchwartz.lean
@@ -28,9 +28,8 @@ namespace SchwartzMap
 
 variable
   (𝕜 : Type*) [RCLike 𝕜]
-  {W : Type*} [NormedAddCommGroup W] [NormedSpace ℂ W] [NormedSpace 𝕜 W]
+  {W : Type*} [NormedAddCommGroup W]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E]
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F]
   {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
   [MeasurableSpace V] [BorelSpace V]
 
@@ -158,6 +157,20 @@ alias fourierTransformCLE_symm_apply := FourierTransform.fourierCLE_symm_apply
 
 end definition
 
+section eval
+
+variable {𝕜' : Type*} [NormedField 𝕜']
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [NormedSpace 𝕜' G] [SMulCommClass ℝ 𝕜' G]
+
+variable (𝕜') in
+theorem fourier_evalCLM_eq (f : 𝓢(V, F →L[ℝ] G)) (m : F) :
+    𝓕 (SchwartzMap.evalCLM 𝕜' F G m f) = SchwartzMap.evalCLM 𝕜' F G m (𝓕 f) := by
+  ext x
+  exact (fourier_continuousLinearMap_apply f.integrable).symm
+
+end eval
+
 section fubini
 
 variable
@@ -192,9 +205,7 @@ theorem integral_fourier_mul_eq (f : 𝓢(V, ℂ)) (g : 𝓢(V, ℂ)) :
 Version where the multiplication is replaced by a general bilinear form `M`. -/
 theorem integral_bilin_fourierInv_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L[ℂ] F →L[ℂ] G) :
     ∫ ξ, M (𝓕⁻ f ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ g x) := by
-  convert (integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm
-  · exact (FourierTransform.fourier_fourierInv_eq g).symm
-  · exact (FourierTransform.fourier_fourierInv_eq f).symm
+  simpa using (integral_bilin_fourier_eq (𝓕⁻ f) (𝓕⁻ g) M).symm
 
 /-- The inverse Fourier transform satisfies `∫ 𝓕⁻ f • g = ∫ f • 𝓕⁻ g`, i.e., it is self-adjoint. -/
 theorem integral_fourierInv_smul_eq (f : 𝓢(V, ℂ)) (g : 𝓢(V, F)) :
@@ -223,6 +234,69 @@ theorem integral_sesq_fourier_fourier (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E 
 
 end fubini
 
+section deriv
+
+theorem fderivCLM_fourier_eq (f : 𝓢(V, E)) :
+    fderivCLM 𝕜 V E (𝓕 f) = 𝓕 (-(2 * π * Complex.I) • smulRightCLM ℂ E (innerSL ℝ) f) := by
+  ext1 x
+  calc
+    _ = fderiv ℝ (𝓕 (f : V → E)) x := by simp [fourier_coe]
+    _ = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) (f : V → E)) x := by
+      rw [Real.fderiv_fourier f.integrable]
+      convert f.integrable_pow_mul volume 1
+      simp
+
+theorem fourier_fderivCLM_eq (f : 𝓢(V, E)) :
+    𝓕 (fderivCLM 𝕜 V E f) = -(2 * π * Complex.I) • smulRightCLM ℂ E (-innerSL ℝ) (𝓕 f) := by
+  ext1 x
+  change 𝓕 (fderiv ℝ (f : V → E)) x = VectorFourier.fourierSMulRight (-innerSL ℝ) (𝓕 (f : V → E)) x
+  rw [Real.fourier_fderiv f.integrable f.differentiable (fderivCLM ℝ V E f).integrable]
+
+open LineDeriv
+
+theorem lineDerivOp_fourier_eq (f : 𝓢(V, E)) (m : V) :
+    ∂_{m} (𝓕 f) = 𝓕 (-(2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) f) := calc
+  _ = SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E (𝓕 f)) := rfl
+  _ = SchwartzMap.evalCLM ℝ V E m (𝓕 (-(2 * π * Complex.I) • smulRightCLM ℂ E (innerSL ℝ) f)) := by
+    rw [fderivCLM_fourier_eq]
+  _ = 𝓕 (SchwartzMap.evalCLM ℝ V E m (-(2 * π * Complex.I) • smulRightCLM ℂ E (innerSL ℝ) f)) := by
+    rw [fourier_evalCLM_eq ℝ (-(2 * π * Complex.I) • smulRightCLM ℂ E (innerSL ℝ) f) m]
+  _ = _ := by
+    congr
+    ext x
+    have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
+    simp [this, innerSL_apply_apply ℝ]
+
+theorem fourier_lineDerivOp_eq (f : 𝓢(V, E)) (m : V) :
+    𝓕 (∂_{m} f) = (2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) (𝓕 f) := calc
+  _ = 𝓕 (SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E f)) := rfl
+  _ = SchwartzMap.evalCLM ℝ V E m (𝓕 (fderivCLM ℝ V E f)) := by
+    rw [fourier_evalCLM_eq ℝ]
+  _ = SchwartzMap.evalCLM ℝ V E m (-(2 * π * Complex.I) • smulRightCLM ℂ E (-innerSL ℝ) (𝓕 f)) := by
+    rw [fourier_fderivCLM_eq]
+  _ = _ := by
+    ext x
+    have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
+    simp [this, innerSL_apply_apply ℝ]
+
+variable [CompleteSpace E]
+
+theorem lineDerivOp_fourierInv_eq (f : 𝓢(V, E)) (m : V) :
+    ∂_{m} (𝓕⁻ f) = 𝓕⁻ ((2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) f) := calc
+  _ = 𝓕⁻ (𝓕 (∂_{m} (𝓕⁻ f))) := by simp
+  _ = 𝓕⁻ ((2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) (𝓕 (𝓕⁻ f))) := by
+    rw [fourier_lineDerivOp_eq]
+  _ = _ := by simp
+
+theorem fourierInv_lineDerivOp_eq (f : 𝓢(V, E)) (m : V) :
+    𝓕⁻ (∂_{m} f) = -(2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) (𝓕⁻ f) := calc
+  _ = 𝓕⁻ (∂_{m} (𝓕 (𝓕⁻ f))) := by simp
+  _ = 𝓕⁻ (𝓕 (-(2 * π * Complex.I) • smulLeftCLM E (inner ℝ · m) (𝓕⁻ f))) := by
+    rw [lineDerivOp_fourier_eq]
+  _ = _ := by simp
+
+end deriv
+
 section L2
 
 variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
diff --git a/Mathlib/Analysis/Distribution/Laplacian.lean b/Mathlib/Analysis/Distribution/Laplacian.lean
new file mode 100644
index 00000000000000..88eb600ce3ad9f
--- /dev/null
+++ b/Mathlib/Analysis/Distribution/Laplacian.lean
@@ -0,0 +1,176 @@
+/-
+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 and tempered distributions -/
+
+@[expose] public noncomputable section
+
+variable {ι 𝕜 R E F F₁ F₂ F₃ V₁ V₂ V₃ : Type*}
+
+namespace LineDeriv
+
+variable [Ring R]
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃]
+
+section Add
+
+variable (E) in
+def laplacian [AddCommGroup V₃] (f : V₁) : V₃ :=
+  ∑ i, lineDerivOp (stdOrthonormalBasis ℝ E i) (lineDerivOp (stdOrthonormalBasis ℝ E i) f)
+
+end Add
+
+section ContinuousLinearMap
+
+variable
+  [AddCommGroup V₁] [Module R V₁] [TopologicalSpace V₁]
+  [AddCommGroup V₂] [Module R V₂] [TopologicalSpace V₂]
+  [AddCommGroup V₃] [Module R 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
+def laplacianCLM : V₁ →L[R] V₃ :=
+  ∑ i, lineDerivOpCLM R V₂ (stdOrthonormalBasis ℝ E i) ∘L
+    lineDerivOpCLM R V₁ (stdOrthonormalBasis ℝ E i)
+
+theorem laplacianCLM_apply (f : V₁) : laplacianCLM R E V₁ f = laplacian E f := by
+  simp [laplacianCLM, laplacian]
+
+end ContinuousLinearMap
+
+end LineDeriv
+
+variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  [NormedAddCommGroup F]
+
+namespace SchwartzMap
+
+variable [NormedSpace ℝ F]
+
+open Laplacian LineDeriv
+
+instance instLaplacian : Laplacian 𝓢(E, F) 𝓢(E, F) where
+  laplacian := LineDeriv.laplacian E
+
+theorem laplacian_eq_sum' (f : 𝓢(E, F)) :
+    Δ f = ∑ i, ∂_{stdOrthonormalBasis ℝ E i} (∂_{stdOrthonormalBasis ℝ E i} f) := rfl
+
+@[simp]
+theorem laplacianCLM_apply [RCLike 𝕜] [NormedSpace 𝕜 F] (f : 𝓢(E, F)) :
+    laplacianCLM 𝕜 E 𝓢(E, F) f = Δ f :=
+  LineDeriv.laplacianCLM_apply f
+
+theorem coe_laplacian_eq_sum [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : 𝓢(E, F)) :
+    Δ (f : E → F) = ∑ i, ∂_{b i} (∂_{b i} f) := by
+  ext x
+  simp only [InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f b,
+    sum_apply]
+  congr 1
+  ext i
+  rw [← iteratedLineDerivOp_eq_iteratedFDeriv]
+  rfl
+
+theorem laplacian_apply (f : 𝓢(E, F)) (x : E) : Δ f x = Δ (f : E → F) x := by
+  rw [coe_laplacian_eq_sum (stdOrthonormalBasis ℝ E), laplacian_eq_sum']
+
+theorem laplacian_eq_sum [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : 𝓢(E, F)) :
+    Δ f = ∑ i, ∂_{b i} (∂_{b i} f) := by
+  ext x
+  rw [laplacian_apply, coe_laplacian_eq_sum b]
+
+open MeasureTheory
+
+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', 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
+
+namespace TemperedDistribution
+
+open Laplacian LineDeriv
+open scoped SchwartzMap
+
+variable [NormedSpace ℂ F]
+
+instance instLaplacian : Laplacian 𝓢'(E, F) 𝓢'(E, F) where
+  laplacian := LineDeriv.laplacian E
+
+theorem laplacian_eq_sum' (f : 𝓢'(E, F)) :
+    Δ f = ∑ i, ∂_{stdOrthonormalBasis ℝ E i} (∂_{stdOrthonormalBasis ℝ E i} f) := rfl
+
+@[simp]
+theorem laplacianCLM_apply (f : 𝓢'(E, F)) : laplacianCLM ℂ E 𝓢'(E, F) f = Δ f :=
+  LineDeriv.laplacianCLM_apply f
+
+@[simp]
+theorem laplacian_apply_apply (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)) : (Δ f) u = f (Δ u) := by
+  simp [laplacian_eq_sum', SchwartzMap.laplacian_eq_sum', UniformConvergenceCLM.sum_apply, map_neg,
+    neg_neg]
+
+theorem laplacian_eq_sum [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : 𝓢'(E, F)) :
+    Δ f = ∑ i, ∂_{b i} (∂_{b i} f) := by
+  ext u
+  simp [UniformConvergenceCLM.sum_apply, map_neg, SchwartzMap.laplacian_eq_sum b]
+
+variable [MeasurableSpace E] [BorelSpace E]
+
+/-- The distributional Laplacian and the classical Laplacian coincide on `𝓢(E, F)`. -/
+@[simp]
+theorem laplacian_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
+    Δ (f : 𝓢'(E, F)) = Δ f := by
+  ext u
+  simp [SchwartzMap.integral_smul_laplacian_right_eq_left]
+
+end TemperedDistribution
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
index 46928e072c7fba..07007969698f42 100644
--- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean
+++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -5,7 +5,6 @@ Authors: Moritz Doll
 -/
 module
 
-public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import Mathlib.Analysis.Normed.Group.ZeroAtInfty
@@ -14,7 +13,6 @@ public import Mathlib.Analysis.SpecialFunctions.Pow.Real
 public import Mathlib.Analysis.Distribution.DerivNotation
 public import Mathlib.Analysis.Distribution.TemperateGrowth
 public import Mathlib.Topology.Algebra.UniformFilterBasis
-public import Mathlib.MeasureTheory.Integral.IntegralEqImproper
 public import Mathlib.MeasureTheory.Function.L2Space
 
 /-!
@@ -630,10 +628,12 @@ end CLM
 
 section EvalCLM
 
-variable [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+variable [NormedField 𝕜]
+variable [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G]
 
+variable (𝕜 F G) in
 /-- The map applying a vector to Hom-valued Schwartz function as a continuous linear map. -/
-protected def evalCLM (m : E) : 𝓢(E, E →L[ℝ] F) →L[𝕜] 𝓢(E, F) :=
+protected def evalCLM (m : F) : 𝓢(E, F →L[ℝ] G) →L[𝕜] 𝓢(E, G) :=
   mkCLM (fun f x => f x m) (fun _ _ _ => rfl) (fun _ _ _ => rfl)
     (fun f => ContDiff.clm_apply f.2 contDiff_const) <| by
   rintro ⟨k, n⟩
@@ -649,6 +649,10 @@ protected def evalCLM (m : E) : 𝓢(E, E →L[ℝ] F) →L[𝕜] 𝓢(E, F) :=
       gcongr
       apply le_seminorm
 
+@[simp]
+theorem evalCLM_apply_apply (f : 𝓢(E, F →L[ℝ] G)) (m : F) (x : E) :
+    SchwartzMap.evalCLM 𝕜 F G m f x = f x m := rfl
+
 end EvalCLM
 
 section Multiplication
@@ -1031,21 +1035,21 @@ theorem hasFDerivAt (f : 𝓢(E, F)) (x : E) : HasFDerivAt f (fderiv ℝ f x) x
 /-- The partial derivative (or directional derivative) in the direction `m : E` as a
 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
+  lineDerivOp m f := (SchwartzMap.evalCLM ℝ E F m ∘L fderivCLM ℝ E F) f
 
 instance instLineDerivAdd : LineDerivAdd E 𝓢(E, F) 𝓢(E, F) where
-  lineDerivOp_add m := ((SchwartzMap.evalCLM m).comp (fderivCLM ℝ E F)).map_add
+  lineDerivOp_add m := (SchwartzMap.evalCLM ℝ E F m ∘L fderivCLM ℝ E F).map_add
 
 instance instLineDerivSMul : LineDerivSMul 𝕜 E 𝓢(E, F) 𝓢(E, F) where
-  lineDerivOp_smul m := ((SchwartzMap.evalCLM m).comp (fderivCLM 𝕜 E F)).map_smul
+  lineDerivOp_smul m := (SchwartzMap.evalCLM 𝕜 E F m ∘L fderivCLM 𝕜 E F).map_smul
 
 instance instContinuousLineDeriv : ContinuousLineDeriv E 𝓢(E, F) 𝓢(E, F) where
-  continuous_lineDerivOp m := ((SchwartzMap.evalCLM m).comp (fderivCLM ℝ E F)).continuous
+  continuous_lineDerivOp m := (SchwartzMap.evalCLM ℝ E F m ∘L fderivCLM ℝ E F).continuous
 
 open LineDeriv
 
 theorem lineDerivOpCLM_eq (m : E) :
-    lineDerivOpCLM 𝕜 𝓢(E, F) m = (SchwartzMap.evalCLM m).comp (fderivCLM 𝕜 E F) := rfl
+    lineDerivOpCLM 𝕜 𝓢(E, F) m = SchwartzMap.evalCLM 𝕜 E F m ∘L fderivCLM 𝕜 E F := rfl
 
 @[deprecated (since := "2025-11-25")]
 alias pderivCLM := lineDerivOpCLM
diff --git a/Mathlib/Analysis/Distribution/Sobolev.lean b/Mathlib/Analysis/Distribution/Sobolev.lean
new file mode 100644
index 00000000000000..fefae7626baf04
--- /dev/null
+++ b/Mathlib/Analysis/Distribution/Sobolev.lean
@@ -0,0 +1,422 @@
+/-
+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.FourierMultiplier
+public import Mathlib.Analysis.Fourier.LpSpace
+
+/-! # Sobolev spaces (Bessel potential spaces)
+
+-/
+
+@[expose] public noncomputable section
+
+variable {E F : Type*}
+  [NormedAddCommGroup E] [NormedAddCommGroup F]
+  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+
+open FourierTransform TemperedDistribution ENNReal MeasureTheory
+open scoped SchwartzMap
+
+section BesselPotential
+
+section normed
+
+variable [NormedSpace ℂ F]
+
+variable (E F) in
+def besselPotential (s : ℝ) : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
+  fourierMultiplierCLM F (fun (x : E) ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ))
+
+variable (E F) in
+@[simp]
+theorem besselPotential_zero : besselPotential E F 0 = ContinuousLinearMap.id ℂ _ := by
+  ext f
+  simp [besselPotential]
+
+@[simp]
+theorem besselPotential_besselPotential_apply (s s' : ℝ) (f : 𝓢'(E, F)) :
+    besselPotential E F s' (besselPotential E F s f) = besselPotential E F (s + s') f := by
+  simp_rw [besselPotential]
+  rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
+  congr
+  ext x
+  simp only [Pi.mul_apply]
+  norm_cast
+  calc
+    _ = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2) := by
+      rw [← Real.rpow_add (by positivity)]
+    _ = _ := by congr; ring
+
+theorem besselPotential_compL_besselPotential (s s' : ℝ) :
+    besselPotential E F s' ∘L besselPotential E F s = besselPotential E F (s + s') := by
+  ext1 f
+  exact besselPotential_besselPotential_apply s s' f
+
+open scoped Real Laplacian
+
+theorem besselPotential_neg_two_laplacian_eq (f : 𝓢'(E, F)) :
+    ((besselPotential E F (-2)) (Δ f)) = fourierMultiplierCLM F (fun x ↦ Complex.ofReal <|
+      -(2 * π) ^ 2 * ‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1 : ℝ)) f := calc
+  _ = -(2 * π) ^ 2 • (fourierMultiplierCLM F
+      (fun x ↦ Complex.ofReal <| (‖x‖ ^ 2) * (1 + ‖x‖ ^ 2) ^ (- (1 : ℝ)))) f := by
+    rw [laplacian_eq_fourierMultiplierCLM, besselPotential,
+      ContinuousLinearMap.map_smul_of_tower,
+      fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
+    congr
+    ext x
+    simp
+  _ = _ := by
+    rw [← Complex.coe_smul, ← fourierMultiplierCLM_smul_apply (by fun_prop)]
+    congr
+    ext x
+    simp [mul_assoc]
+
+end normed
+
+section inner
+
+variable [InnerProductSpace ℂ F]
+
+open FourierTransform
+
+@[simp]
+theorem fourier_besselPotential_eq_smulLeftCLM_fourierInv_apply (s : ℝ) (f : 𝓢'(E, F)) :
+    𝓕 (besselPotential E F s f) =
+      smulLeftCLM F (fun x : E ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) (𝓕 f) := by
+  simp [besselPotential, fourierMultiplierCLM]
+
+end inner
+
+end BesselPotential
+
+section normed
+
+variable [NormedSpace ℂ F] [CompleteSpace F]
+
+def MemSobolev (s : ℝ) (p : ℝ≥0∞) [hp : Fact (1 ≤ p)] (f : 𝓢'(E, F)) : Prop :=
+  ∃ (f' : Lp F p (volume : Measure E)),
+    besselPotential E F s f = f'
+
+theorem memSobolev_zero_iff {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] {f : 𝓢'(E, F)} : MemSobolev 0 p f ↔
+    ∃ (f' : Lp F p (volume : Measure E)), f = f' := by
+  simp [MemSobolev]
+
+theorem memSobolev_add {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] {f g : 𝓢'(E, F)}
+    (hf : MemSobolev s p f) (hg : MemSobolev s p g) : MemSobolev s p (f + g) := by
+  obtain ⟨f', hf⟩ := hf
+  obtain ⟨g', hg⟩ := hg
+  use f' + g'
+  change _ = Lp.toTemperedDistributionCLM F volume p (f' + g')
+  simp [map_add, hf, hg]
+
+theorem memSobolev_smul {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] (c : ℂ) {f : 𝓢'(E, F)}
+    (hf : MemSobolev s p f) : MemSobolev s p (c • f) := by
+  obtain ⟨f', hf⟩ := hf
+  use c • f'
+  change _ = Lp.toTemperedDistributionCLM F volume p (c • f')
+  simp [hf]
+
+variable (E F) in
+theorem memSobolev_zero (s : ℝ) (p : ℝ≥0∞) [hp : Fact (1 ≤ p)] : MemSobolev s p (0 : 𝓢'(E, F)) := by
+  use 0
+  change _ = Lp.toTemperedDistributionCLM F volume p 0
+  simp only [map_zero]
+
+@[simp]
+theorem memSobolev_besselPotential_iff {s r : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] {f : 𝓢'(E, F)} :
+    MemSobolev s p (besselPotential E F r f) ↔ MemSobolev (r + s) p f := by
+  simp [MemSobolev]
+
+/-- Schwartz functions are in every Sobolev space. -/
+theorem memSobolev_toTemperedDistributionCLM {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] (f : 𝓢(E, F)) :
+    MemSobolev s p (f : 𝓢'(E, F)) := by
+  use (SchwartzMap.fourierMultiplierCLM F (fun (x : E) ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) f).toLp p
+  rw [besselPotential, Lp.toTemperedDistribution_toLp_eq,
+    fourierMultiplierCLM_toTemperedDistributionCLM_eq (by fun_prop)]
+  congr 1
+  apply SchwartzMap.fourierMultiplierCLM_ofReal ℂ
+    (Function.hasTemperateGrowth_one_add_norm_sq_rpow E (s / 2))
+
+variable (E F) in
+structure Sobolev (s : ℝ) (p : ℝ≥0∞) [hp : Fact (1 ≤ p)] where
+  toDistr : 𝓢'(E, F)
+  sobFn : Lp F p (volume : Measure E)
+  bessel_toDistr_eq_sobFn : besselPotential E F s toDistr = sobFn
+
+namespace Sobolev
+
+variable {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)]
+
+theorem ext' {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] {f g : Sobolev E F s p}
+    (h₁ : f.toDistr = g.toDistr) (h₂ : f.sobFn = g.sobFn) : f = g := by
+  cases f; cases g; congr
+
+theorem memSobolev_toDistr (f : Sobolev E F s p) : MemSobolev s p f.toDistr :=
+  ⟨f.sobFn, f.bessel_toDistr_eq_sobFn⟩
+
+@[simp]
+theorem besselPotential_neg_sobFn_eq {f : Sobolev E F s p} :
+    besselPotential E F (-s) f.sobFn = f.toDistr := by
+  simp [← f.bessel_toDistr_eq_sobFn]
+
+@[ext]
+theorem ext {s : ℝ} {p : ℝ≥0∞} [hp : Fact (1 ≤ p)] {f g : Sobolev E F s p}
+    (h₁ : f.toDistr = g.toDistr) : f = g := by
+  apply ext' h₁
+  apply_fun MeasureTheory.Lp.toTemperedDistribution; swap
+  · apply LinearMap.ker_eq_bot.mp MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot
+  calc
+    f.sobFn = besselPotential E F s f.toDistr := f.bessel_toDistr_eq_sobFn.symm
+    _ = besselPotential E F s g.toDistr := by congr
+    _ = g.sobFn := g.bessel_toDistr_eq_sobFn
+
+def _root_.MemSobolev.toSobolev {f : 𝓢'(E, F)} (hf : MemSobolev s p f) : Sobolev E F s p where
+  toDistr := f
+  sobFn := hf.choose
+  bessel_toDistr_eq_sobFn := hf.choose_spec
+
+@[simp]
+theorem _root_.MemSobolev.toSobolev_toDistr {f : 𝓢'(E, F)} (hf : MemSobolev s p f) :
+    hf.toSobolev.toDistr = f := rfl
+
+theorem _root_.MemSobolev.toSobolev_injective {f g : 𝓢'(E, F)} (hf : MemSobolev s p f)
+    (hg : MemSobolev s p g) (h : hf.toSobolev = hg.toSobolev) : f = g := by
+  rw [← hf.toSobolev_toDistr, ← hg.toSobolev_toDistr, h]
+
+variable (E F s p) in
+theorem injective_sobFn :
+    Function.Injective (sobFn (s := s) (p := p) (E := E) (F := F)) := by
+  intro f g hfg
+  refine ext' ?_ hfg
+  calc
+    f.toDistr = besselPotential E F (-s) (Sobolev.sobFn f) := by simp
+    _ = besselPotential E F (-s) (Sobolev.sobFn g) := by congr
+    _ = g.toDistr := by simp
+
+instance instZero : Zero (Sobolev E F s p) where
+  zero := {
+    toDistr := 0
+    sobFn := 0
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p _
+      simp [-Lp.toTemperedDistributionCLM_apply] }
+
+instance instAdd : Add (Sobolev E F s p) where
+  add f g := {
+    toDistr := f.toDistr + g.toDistr
+    sobFn := f.sobFn + g.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p (_ + _)
+      simp [map_add, f.bessel_toDistr_eq_sobFn, g.bessel_toDistr_eq_sobFn] }
+
+@[simp]
+theorem toDistr_add (f g : Sobolev E F s p) : (f + g).toDistr = f.toDistr + g.toDistr := rfl
+
+instance instSub : Sub (Sobolev E F s p) where
+  sub f g := {
+    toDistr := f.toDistr - g.toDistr
+    sobFn := f.sobFn - g.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p (_ - _)
+      simp [map_sub, f.bessel_toDistr_eq_sobFn, g.bessel_toDistr_eq_sobFn] }
+
+instance instNeg : Neg (Sobolev E F s p) where
+  neg f := {
+    toDistr := -f.toDistr
+    sobFn := -f.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p (- _)
+      simp [map_neg, f.bessel_toDistr_eq_sobFn] }
+
+instance instNSMul : SMul ℕ (Sobolev E F s p) where
+  smul c f := {
+    toDistr := c • f.toDistr
+    sobFn := c • f.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p _
+      simp [f.bessel_toDistr_eq_sobFn] }
+
+instance instZSMul : SMul ℤ (Sobolev E F s p) where
+  smul c f := {
+    toDistr := c • f.toDistr
+    sobFn := c • f.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p _
+      simp [f.bessel_toDistr_eq_sobFn] }
+
+/- Generalize this-/
+instance instSMul : SMul ℂ (Sobolev E F s p) where
+  smul c f := {
+    toDistr := c • f.toDistr
+    sobFn := c • f.sobFn
+    bessel_toDistr_eq_sobFn := by
+      change _ = Lp.toTemperedDistributionCLM F volume p _
+      simp [map_smul, f.bessel_toDistr_eq_sobFn] }
+
+@[simp]
+theorem toDistr_smul (c : ℂ) (f : Sobolev E F s p) : (c • f).toDistr = c • f.toDistr := rfl
+
+instance instAddCommGroup : AddCommGroup (Sobolev E F s p) :=
+  (injective_sobFn E F s p).addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
+variable (E F s p) in
+/-- Coercion as an additive homomorphism. -/
+def coeHom : Sobolev E F s p →+ 𝓢'(E, F) where
+  toFun f := f.toDistr
+  map_zero' := rfl
+  map_add' _ _ := rfl
+
+theorem coeHom_injective : Function.Injective (coeHom E F s p) := by
+  apply ext
+
+instance instModule : Module ℂ (Sobolev E F s p) :=
+  coeHom_injective.module ℂ (coeHom E F s p) fun _ _ => rfl
+
+variable (E F s p) in
+def toLpₗ : Sobolev E F s p →ₗ[ℂ] Lp F p (volume : Measure E) where
+  toFun := sobFn
+  map_add' f g := by rfl
+  map_smul' c f := by rfl
+
+@[simp]
+theorem toLpₗ_apply (f : Sobolev E F s p) :
+    toLpₗ E F s p f = sobFn f := rfl
+
+theorem sobFn_add (f g : Sobolev E F s p) :
+    sobFn (f + g) = sobFn f + sobFn g := rfl
+
+theorem sobFn_smul (c : ℂ) (f : Sobolev E F s p) :
+    sobFn (c • f) = c • sobFn f := rfl
+
+instance instNormedAddCommGroup :
+    NormedAddCommGroup (Sobolev E F s p) :=
+  NormedAddCommGroup.induced (Sobolev E F s p) (Lp F p (volume : Measure E)) (toLpₗ E F s p)
+    (injective_sobFn E F s p)
+
+@[simp]
+theorem norm_sobFn_eq (f : Sobolev E F s p) : ‖f.sobFn‖ = ‖f‖ :=
+  rfl
+
+instance instNormedSpace :
+    NormedSpace ℂ (Sobolev E F s p) where
+  norm_smul_le c f := by
+    simp_rw [← norm_sobFn_eq, ← norm_smul]
+    rfl
+
+variable (E F s p) in
+def toLpₗᵢ :
+    Sobolev E F s p →ₗᵢ[ℂ] Lp F p (volume : Measure E) where
+  __ := toLpₗ E F s p
+  norm_map' _ := rfl
+
+end Sobolev
+
+end normed
+
+section inner
+
+variable [InnerProductSpace ℂ F] [CompleteSpace F]
+
+theorem memSobolev_two_iff_fourier {s : ℝ} {f : 𝓢'(E, F)} :
+    MemSobolev s 2 f ↔ ∃ (f' : Lp F 2 (volume : Measure E)),
+    smulLeftCLM F (fun (x : E) ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) (𝓕 f) = f' := by
+  rw [MemSobolev]
+  constructor
+  · intro ⟨f', hf'⟩
+    use 𝓕 f'
+    apply_fun 𝓕 at hf'
+    rw [fourier_besselPotential_eq_smulLeftCLM_fourierInv_apply] at hf'
+    rw [hf', Lp.fourier_toTemperedDistribution_eq f']
+  · intro ⟨f', hf'⟩
+    use 𝓕⁻ f'
+    rw [besselPotential, TemperedDistribution.fourierMultiplierCLM_apply]
+    apply_fun 𝓕⁻ at hf'
+    rw [hf', Lp.fourierInv_toTemperedDistribution_eq f']
+
+theorem memSobolev_zero_two_iff_fourierTransform {f : 𝓢'(E, F)} :
+    MemSobolev 0 2 f ↔ ∃ (f' : Lp F 2 (volume : Measure E)), 𝓕 f = f' := by
+  simp [memSobolev_two_iff_fourier]
+
+open scoped BoundedContinuousFunction
+
+theorem memSobolev_fourierMultiplierCLM_bounded {s : ℝ} {g : E → ℂ} (hg₁ : g.HasTemperateGrowth)
+    (hg₂ : ∃ C, ∀ x, ‖g x‖ ≤ C) {f : 𝓢'(E, F)} (hf : MemSobolev s 2 f) :
+    MemSobolev s 2 (fourierMultiplierCLM F g f) := by
+  rw [memSobolev_two_iff_fourier] at hf ⊢
+  obtain ⟨f', hf⟩ := hf
+  obtain ⟨C, hC⟩ := hg₂
+  set g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g hg₁.1.continuous C hC
+  use (g'.memLp_top.toLp _ (μ := volume)) • f'
+  rw [MeasureTheory.Lp.toTemperedDistribution_smul_eq (by apply hg₁), ← hf,
+    fourierMultiplierCLM_apply, fourier_fourierInv_eq,
+    smulLeftCLM_smulLeftCLM_apply hg₁ (by fun_prop),
+    smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by apply hg₁)]
+  congr 2
+  ext x
+  rw [mul_comm]
+  congr
+
+section LineDeriv
+
+open scoped LineDeriv Laplacian Real
+
+/-- The Laplacian maps `H^{s}` to `H^{s - 2}`.
+
+The other implication is slightly harder :-) -/
+theorem MemSobolev.laplacian {s : ℝ} {f : 𝓢'(E, F)} (hf : MemSobolev s 2 f) :
+    MemSobolev (s - 2) 2 (Δ f) := by
+  rw [SubNegMonoid.sub_eq_add_neg s 2, add_comm, ← memSobolev_besselPotential_iff,
+    besselPotential_neg_two_laplacian_eq f]
+  apply memSobolev_fourierMultiplierCLM_bounded (by fun_prop) _ hf
+  use (2 * π) ^ 2
+  intro x
+  rw [Real.rpow_neg (by positivity)]
+  norm_cast
+  simp only [pow_one, norm_mul, norm_pow, norm_inv, Real.norm_eq_abs]
+  simp only [abs_neg, abs_pow, abs_mul, Nat.abs_ofNat, abs_norm]
+  have : 0 < π := by positivity
+  rw [abs_of_pos this]
+  rw [mul_inv_le_iff₀]
+  · gcongr
+    grind
+  norm_cast
+  positivity
+
+end LineDeriv
+
+namespace Sobolev
+
+instance instInnerProductSpace (s : ℝ) :
+    InnerProductSpace ℂ (Sobolev E F s 2) where
+  inner f g := inner ℂ f.sobFn g.sobFn
+  norm_sq_eq_re_inner f := by simp; norm_cast
+  conj_inner_symm f g := by simp
+  add_left f g h := by rw [sobFn_add, inner_add_left]
+  smul_left f g c := by rw [sobFn_smul, inner_smul_left]
+
+open Laplacian
+
+instance instLaplacian (s : ℝ) : Laplacian (Sobolev E F s 2) (Sobolev E F (s - 2) 2) where
+  laplacian f := f.memSobolev_toDistr.laplacian.toSobolev
+
+@[simp]
+theorem laplacian_toDistr {s : ℝ} (f : Sobolev E F s 2) : (Δ f).toDistr = Δ f.toDistr := rfl
+
+def laplacianₗ {s : ℝ} : Sobolev E F s 2 →ₗ[ℂ] Sobolev E F (s - 2) 2 where
+  toFun := Δ
+  map_add' f g := by
+    ext1
+    simpa using (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_add f.toDistr g.toDistr
+  map_smul' c f := by
+    ext1
+    simpa only [laplacian_toDistr, laplacianCLM_apply] using
+      (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_smul c f.toDistr
+
+end Sobolev
+
+end inner
diff --git a/Mathlib/Analysis/Distribution/TemperedDistribution.lean b/Mathlib/Analysis/Distribution/TemperedDistribution.lean
index e1c97d09b603c2..6e100963bbdf3e 100644
--- a/Mathlib/Analysis/Distribution/TemperedDistribution.lean
+++ b/Mathlib/Analysis/Distribution/TemperedDistribution.lean
@@ -252,6 +252,13 @@ theorem smulLeftCLM_smulLeftCLM_apply {g₁ g₂ : E → ℂ} (hg₁ : g₁.HasT
     smulLeftCLM F g₂ (smulLeftCLM F g₁ f) = smulLeftCLM F (g₁ * g₂) f := by
   ext; simp [hg₁, hg₂]
 
+theorem smulLeftCLM_smul {g : E → ℂ} (hg : g.HasTemperateGrowth) (c : ℂ) :
+    smulLeftCLM F (c • g) = c • smulLeftCLM F g := by
+  ext1 f
+  have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop
+  convert (smulLeftCLM_smulLeftCLM_apply this hg f).symm using 1
+  simp
+
 theorem smulLeftCLM_compL_smulLeftCLM {g₁ g₂ : E → ℂ} (hg₁ : g₁.HasTemperateGrowth)
     (hg₂ : g₂.HasTemperateGrowth) :
     smulLeftCLM F g₂ ∘L smulLeftCLM F g₁ = smulLeftCLM F (g₁ * g₂) := by
@@ -404,6 +411,8 @@ instance instFourierPair : FourierPair 𝓢'(E, F) 𝓢'(E, F) where
 instance instFourierPairInv : FourierInvPair 𝓢'(E, F) 𝓢'(E, F) where
   fourier_fourierInv_eq f := by ext; simp
 
+section embedding
+
 variable [CompleteSpace F]
 
 /-- The distributional Fourier transform and the classical Fourier transform coincide on
@@ -423,6 +432,18 @@ theorem fourierInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
     rw [fourier_toTemperedDistributionCLM_eq]
   _ = _ := fourierInv_fourier_eq _
 
+end embedding
+
+open LineDeriv Real
+
+theorem fourier_lineDerivOp_eq (f : 𝓢'(E, F)) (m : E) :
+    𝓕 (∂_{m} f) = (2 * π * Complex.I) • smulLeftCLM F (inner ℝ · m) (𝓕 f) := by
+  ext u
+  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
+  have f_neg : ∀ (x : 𝓢(E, ℂ)), 𝓕 (-x) = -𝓕 x :=
+    (fourierCLM ℂ 𝓢(E, ℂ)).map_neg
+  simp [SchwartzMap.lineDerivOp_fourier_eq, ← smulLeftCLM_ofReal ℂ this, f_neg]
+
 end Fourier
 
 section DiracDelta
diff --git a/Mathlib/Analysis/InnerProductSpace/Laplacian.lean b/Mathlib/Analysis/InnerProductSpace/Laplacian.lean
index 64154c1ac76c8d..86a2506a8f4d7d 100644
--- a/Mathlib/Analysis/InnerProductSpace/Laplacian.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Laplacian.lean
@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Calculus.ContDiff.Basic
 public import Mathlib.Analysis.Calculus.ContDiff.Operations
 public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 public import Mathlib.Analysis.InnerProductSpace.CanonicalTensor
+public import Mathlib.Analysis.Distribution.DerivNotation
 
 /-!
 # The Laplacian
@@ -133,16 +134,14 @@ noncomputable def laplacianWithin : E → F :=
 @[inherit_doc]
 scoped[InnerProductSpace] notation "Δ[" s "] " f:60 => laplacianWithin f s
 
-variable (f) in
-/--
-Laplacian for functions on real inner product spaces. Use `open InnerProductSpace` to access the
-notation `Δ` for `InnerProductSpace.Laplacian`.
--/
-noncomputable def laplacian : E → F :=
-  fun x ↦ tensorIteratedFDerivTwo ℝ f x (InnerProductSpace.canonicalCovariantTensor E)
+noncomputable
+instance instLaplacian : Laplacian (E → F) (E → F) where
+  laplacian f x := tensorIteratedFDerivTwo ℝ f x (InnerProductSpace.canonicalCovariantTensor E)
 
-@[inherit_doc]
-scoped[InnerProductSpace] notation "Δ" => laplacian
+@[deprecated (since := "2025-12-31")]
+alias InnerProduct.laplacian := _root_.Laplacian.laplacian
+
+open Laplacian
 
 /--
 The Laplacian equals the Laplacian with respect to `Set.univ`.
@@ -176,7 +175,7 @@ theorem laplacian_eq_iteratedFDeriv_orthonormalBasis {ι : Type*} [Fintype ι]
     (v : OrthonormalBasis ι ℝ E) :
     Δ f = fun x ↦ ∑ i, iteratedFDeriv ℝ 2 f x ![v i, v i] := by
   ext x
-  simp [InnerProductSpace.laplacian, canonicalCovariantTensor_eq_sum E v,
+  simp [laplacian, canonicalCovariantTensor_eq_sum E v,
     tensorIteratedFDerivTwo_eq_iteratedFDeriv]
 
 variable (f) in