feat: Position & momentum unbounded operators

PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean

@@ -126,8 +126,10 @@ lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j
   rw [positionOperator_apply, momentumOperator_apply_fun]
   rw [momentumOperator_apply, positionOperator_apply_fun]
   simp only [neg_mul, Pi.smul_apply, smul_eq_mul, mul_neg, sub_neg_eq_add]
-
-  have h : (fun x ↦ ↑(x i) * ψ x) = (fun (x : Space d) ↦ x i) • ψ := rfl
+  have h : ⇑(smulLeftCLM ℂ ⇑(Space.coordCLM i) • ψ) = (fun (x : Space d) ↦ x i) • ψ := by
+    ext x
+    rw [ContinuousLinearMap.smul_def, smulLeftCLM_apply_apply (by fun_prop), Space.coordCLM_apply]
+    simp only [Space.coord_apply, Complex.real_smul, Pi.smul_apply']
   rw [h]
   rw [Space.deriv_smul (by fun_prop) (SchwartzMap.differentiableAt ψ)]
   rw [Space.deriv_component, ite_cond_symm j i]

PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean

@@ -3,15 +3,23 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gregory J. Loges
 -/
-import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 import PhysLean.QuantumMechanics.PlanckConstant
+import PhysLean.SpaceAndTime.Space.Derivatives.Basic
 /-!
 
 # Momentum vector operator
 
 In this module we define:
-- The momentum operator on Schwartz maps, component-wise.
-- The momentum squared operator on Schwartz maps.
+- `momentumOperator i` acting on Schwartz maps `𝓢(Space d, ℂ)` as `-Iℏ∂ᵢ`.
+- `momentumOperatorSqr` acting on Schwartz maps `𝓢(Space d, ℂ)` as `∑ᵢ 𝐩[i]∘𝐩[i]`.
+- `momentumUnboundedOperator i`, a symmetric unbounded operator acting on the Schwartz submodule
+  of the Hilbert space `SpaceDHilbertSpace d`.
+
+We also introduce the following notation:
+- `𝐩[i]` for `momentumOperator i`
+- `𝐩²` for `momentumOperatorSqr`
 
 -/
 
@@ -21,33 +29,67 @@ open Constants
 open Space
 open ContDiff SchwartzMap
 
+variable {d : ℕ} (i : Fin d)
+
 /-- Component `i` of the momentum operator is the continuous linear map
 from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `-iℏ ∂ᵢψ`. -/
-def momentumOperator {d : ℕ} (i : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+def momentumOperator : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
   (- Complex.I * ℏ) • (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis i)) ∘L
     (SchwartzMap.fderivCLM ℂ (Space d) ℂ)
 
 @[inherit_doc momentumOperator]
 macro "𝐩[" i:term "]" : term => `(momentumOperator $i)
 
-lemma momentumOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+lemma momentumOperator_apply_fun (ψ : 𝓢(Space d, ℂ)) :
     𝐩[i] ψ = (- Complex.I * ℏ) • ∂[i] ψ := rfl
 
-lemma momentumOperator_apply {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+@[simp]
+lemma momentumOperator_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
     𝐩[i] ψ x = - Complex.I * ℏ * ∂[i] ψ x := rfl
 
 /-- The square of the momentum operator, `𝐩² ≔ ∑ᵢ 𝐩ᵢ∘𝐩ᵢ`. -/
-def momentumOperatorSqr {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := ∑ i, 𝐩[i] ∘L 𝐩[i]
+def momentumOperatorSqr : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := ∑ i, 𝐩[i] ∘L 𝐩[i]
 
 @[inherit_doc momentumOperatorSqr]
 notation "𝐩²" => momentumOperatorSqr
 
-lemma momentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+lemma momentumOperatorSqr_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
     𝐩² ψ x = ∑ i, 𝐩[i] (𝐩[i] ψ) x := by
   dsimp only [momentumOperatorSqr]
   rw [← SchwartzMap.coe_coeHom]
   simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp', Finset.sum_apply,
     Function.comp_apply, map_sum]
 
+/-!
+## Unbounded momentum operators
+-/
+
+open SpaceDHilbertSpace
+
+/-- The momentum operators defined on the Schwartz submodule. -/
+def momentumOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
+  (schwartzEquiv (d := d)) ∘ₗ 𝐩[i].toLinearMap ∘ₗ (schwartzEquiv (d := d)).symm
+
+@[sorryful]
+lemma momentumOperatorSchwartz_isSymmetric : (momentumOperatorSchwartz i).IsSymmetric := by
+  intro ψ ψ'
+  obtain ⟨f, rfl⟩ := schwartzEquiv_exists ψ
+  obtain ⟨f', rfl⟩ := schwartzEquiv_exists ψ'
+  unfold momentumOperatorSchwartz
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, ContinuousLinearMap.coe_coe,
+    Function.comp_apply, LinearEquiv.symm_apply_apply, schwartzEquiv_inner, momentumOperator_apply,
+    neg_mul, map_neg, map_mul, Complex.conj_I, Complex.conj_ofReal, neg_neg, mul_neg]
+  -- Need integration by parts and `starRingEnd ∂[i] = ∂[i] starRingEnd`:
+  -- ⊢ ∫ (x : Space d), Complex.I * ↑↑ℏ * (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
+  -- ∫ (x : Space d), -((starRingEnd ℂ) (f x) * (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x))
+  sorry
+
+/-- The symmetric momentum unbounded operators with domain the Schwartz submodule
+  of the Hilbert space. -/
+@[sorryful]
+def momentumUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (hE := schwartzSubmodule_dense) (momentumOperatorSchwartz i)
+    (momentumOperatorSchwartz_isSymmetric i)
+
 end
 end QuantumMechanics

PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean

@@ -3,14 +3,27 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gregory J. Loges
 -/
+import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 import PhysLean.SpaceAndTime.Space.Derivatives.Basic
 /-!
 
 # Position operators
 
 In this module we define:
-- The position vector operator on Schwartz maps, component-wise.
-- The (regularized) real powers of the radius operator on Schwartz maps.
+- `positionOperator i` acting on Schwartz maps `𝓢(Space d, ℂ)` by multiplication by `xᵢ`.
+- `radiusRegPowOperator ε s` acting on Schwartz maps `𝓢(Space d, ℂ)` by multiplication
+  by `(‖x‖² + ε²)^(s/2)`, a smooth regularization of `‖x‖ˢ`.
+- `positionUnboundedOperator i`, a symmetric unbounded operator acting on the Schwartz submodule
+  of the Hilbert space `SpaceDHilbertSpace d`.
+- `radiusRegPowUnboundedOperator ε s`, a symmetric unbounded operator acting on the Schwartz
+  submodule of the Hilbert space `SpaceDHilbertSpace d`. For `s ≤ 0` this operator is bounded
+  (by `ε⁻ˢ`) and has natural domain the entire Hilbert space, but for uniformity we use the same
+  domain for all `s`.
+
+We also introduce the following notation:
+- `𝐱[i]` for `positionOperator i`
+- `𝐫[ε,s]` for `radiusRegPowOperator ε s`
 
 -/
 
@@ -19,45 +32,47 @@ noncomputable section
 open Space
 open Function SchwartzMap ContDiff
 
-/-
+variable {d : ℕ} (i : Fin d)
+
+/-!
 ## Position vector operator
 -/
 
 /-- Component `i` of the position operator is the continuous linear map
-from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `xᵢψ`. -/
-def positionOperator (i : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
-  SchwartzMap.smulLeftCLM ℂ (Complex.ofReal ∘ coordCLM i)
+  from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `xᵢψ`. -/
+def positionOperator : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  SchwartzMap.smulLeftCLM ℂ (Complex.ofRealCLM ∘L coordCLM i)
 
 @[inherit_doc positionOperator]
 macro "𝐱[" i:term "]" : term => `(positionOperator $i)
 
-lemma positionOperator_apply_fun (i : Fin d) (ψ : 𝓢(Space d, ℂ)) :
-    𝐱[i] ψ = (fun x ↦ x i * ψ x) := by
+lemma positionOperator_apply_fun (ψ : 𝓢(Space d, ℂ)) :
+    𝐱[i] ψ = smulLeftCLM ℂ (coordCLM i) • ψ := by
   unfold positionOperator
   ext x
-  rw [SchwartzMap.smulLeftCLM_apply_apply]
-  · rw [Function.comp_apply, smul_eq_mul]
-    rw [coordCLM_apply, coord_apply]
-  · fun_prop
+  simp [smulLeftCLM_apply_apply (g := Complex.ofRealCLM ∘ (coordCLM i)) (by fun_prop) _ _,
+    smulLeftCLM_apply (g := coordCLM i) (by fun_prop) _]
 
-lemma positionOperator_apply (i : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
-    𝐱[i] ψ x = x i * ψ x := by rw [positionOperator_apply_fun]
+@[simp]
+lemma positionOperator_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐱[i] ψ x = x i * ψ x := by
+  simp [positionOperator_apply_fun, smulLeftCLM_apply (g := coordCLM i) (by fun_prop) _,
+    coordCLM_apply, coord_apply]
 
-/-
+/-!
 
 ## Radius operator
 
 -/
 TODO "ZGCNP" "Incorporate normRegularizedPow into Space.Norm"
 
-/-- Power of regularized norm, `(‖x‖² + ε²)^(s/2)` -/
+/-- Power of regularized norm, `(‖x‖² + ε²)^(s/2)`. -/
 private def normRegularizedPow (ε s : ℝ) : Space d → ℝ :=
   fun x ↦ (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)
 
-private lemma normRegularizedPow_hasTemperateGrowth (hε : 0 < ε) :
+private lemma normRegularizedPow_hasTemperateGrowth {ε s : ℝ} (hε : 0 < ε) :
     HasTemperateGrowth (normRegularizedPow (d := d) ε s) := by
   -- Write `normRegularizedPow` as the composition of three simple functions
-  -- to take advantage of `hasTemperateGrowth_one_add_norm_sq_rpow`
+  -- to take advantage of `hasTemperateGrowth_one_add_norm_sq_rpow`.
   let f1 := fun (x : ℝ) ↦ (ε ^ 2) ^ (s / 2) * x
   let f2 := fun (x : Space d) ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)
   let f3 := fun (x : Space d) ↦ ε⁻¹ • x
@@ -85,7 +100,7 @@ def radiusRegPowOperator (ε s : ℝ) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space
 @[inherit_doc radiusRegPowOperator]
 macro "𝐫[" ε:term "," s:term "]" : term => `(radiusRegPowOperator $ε $s)
 
-lemma radiusRegPowOperator_apply_fun (hε : 0 < ε) :
+lemma radiusRegPowOperator_apply_fun {ε s : ℝ} (hε : 0 < ε) {ψ : 𝓢(Space d, ℂ)} :
     𝐫[ε,s] ψ = fun x ↦ (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2) • ψ x := by
   unfold radiusRegPowOperator
   ext x
@@ -94,11 +109,12 @@ lemma radiusRegPowOperator_apply_fun (hε : 0 < ε) :
     rw [comp_apply, smul_eq_mul, Complex.real_smul]
   · exact HasTemperateGrowth.comp (by fun_prop) (normRegularizedPow_hasTemperateGrowth hε)
 
-lemma radiusRegPowOperator_apply (hε : 0 < ε) :
-    𝐫[ε,s] ψ x = (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2) • ψ x := by
+lemma radiusRegPowOperator_apply {ε s : ℝ} (hε : 0 < ε) {ψ : 𝓢(Space d, ℂ)}
+    {x : Space d} : 𝐫[ε,s] ψ x = (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2) • ψ x := by
   rw [radiusRegPowOperator_apply_fun hε]
 
-lemma radiusRegPowOperator_comp_eq (hε : 0 < ε) (s t : ℝ) :
+@[simp]
+lemma radiusRegPowOperator_comp_eq {ε s t : ℝ} (hε : 0 < ε) :
     (radiusRegPowOperator (d := d) ε s) ∘L 𝐫[ε,t] = 𝐫[ε,s+t] := by
   unfold radiusRegPowOperator
   ext ψ x
@@ -113,23 +129,68 @@ lemma radiusRegPowOperator_comp_eq (hε : 0 < ε) (s t : ℝ) :
     · exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_pos hε)
   repeat exact HasTemperateGrowth.comp (by fun_prop) (normRegularizedPow_hasTemperateGrowth hε)
 
-lemma radiusRegPowOperator_zero (hε : 0 < ε) :
+@[simp]
+lemma radiusRegPowOperator_zero {ε : ℝ} (hε : 0 < ε) :
     𝐫[ε,0] = ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by
   ext ψ x
-  rw [radiusRegPowOperator_apply hε, zero_div, Real.rpow_zero, one_smul,
-    ContinuousLinearMap.coe_id', id_eq]
+  simp [radiusRegPowOperator_apply hε]
 
-lemma positionOperatorSqr_eq (hε : 0 < ε) : ∑ i, 𝐱[i] ∘L 𝐱[i] =
+lemma positionOperatorSqr_eq {ε : ℝ} (hε : 0 < ε) : ∑ i, 𝐱[i] ∘L 𝐱[i] =
     𝐫[ε,2] - ε ^ 2 • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by
   ext ψ x
-  simp only [ContinuousLinearMap.coe_sum', Finset.sum_apply, SchwartzMap.sum_apply,
-    ContinuousLinearMap.comp_apply, ContinuousLinearMap.sub_apply, SchwartzMap.sub_apply,
-    ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, SchwartzMap.smul_apply]
-  simp only [positionOperator_apply_fun, radiusRegPowOperator_apply_fun hε]
-  simp only [← mul_assoc, ← Finset.sum_mul, ← Complex.ofReal_mul]
-  rw [div_self (by norm_num), Real.rpow_one, ← sub_smul, add_sub_cancel_right]
-  rw [Space.norm_sq_eq, Complex.real_smul, Complex.ofReal_sum]
-  simp only [pow_two]
+  simp [radiusRegPowOperator_apply hε, Space.norm_sq_eq, ← mul_assoc, ← Finset.sum_mul,
+    add_smul, ← pow_two]
+
+/-!
+## Unbounded position operators
+-/
+
+open SpaceDHilbertSpace
+
+/-- The position operators defined on the Schwartz submodule. -/
+def positionOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
+  (schwartzEquiv (d := d)) ∘ₗ 𝐱[i].toLinearMap ∘ₗ (schwartzEquiv (d := d)).symm
+
+lemma positionOperatorSchwartz_isSymmetric : (positionOperatorSchwartz i).IsSymmetric := by
+  intro ψ ψ'
+  obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ
+  obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ'
+  unfold positionOperatorSchwartz
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, schwartzEquiv_inner]
+  congr with x
+  simp only [LinearEquiv.symm_apply_apply, ContinuousLinearMap.coe_coe,
+    positionOperator_apply, map_mul, Complex.conj_ofReal]
+  ring
+
+/-- The symmetric position unbounded operators with domain the Schwartz submodule
+  of the Hilbert space. -/
+def positionUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (hE := schwartzSubmodule_dense) (positionOperatorSchwartz i)
+    (positionOperatorSchwartz_isSymmetric i)
+
+/-- The (regularized) radius operators defined on the Schwartz submodule. -/
+def radiusRegPowOperatorSchwartz (ε s : ℝ) : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
+  (schwartzEquiv (d := d)) ∘ₗ (radiusRegPowOperator (d := d) ε s).toLinearMap ∘ₗ
+  (schwartzEquiv (d := d)).symm
+
+lemma radiusRegPowOperatorSchwartz_isSymmetric (ε s : ℝ) (hε : 0 < ε) :
+    (radiusRegPowOperatorSchwartz (d := d) ε s).IsSymmetric := by
+  intro ψ ψ'
+  obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ
+  obtain ⟨_, rfl⟩ := schwartzEquiv_exists ψ'
+  unfold radiusRegPowOperatorSchwartz
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, schwartzEquiv_inner]
+  congr with x
+  simp only [LinearEquiv.symm_apply_apply, ContinuousLinearMap.coe_coe,
+    radiusRegPowOperator_apply hε, Complex.real_smul, map_mul, Complex.conj_ofReal]
+  ring
+
+/-- The symmetric (regularized) radius unbounded operators with domain the Schwartz submodule
+  of the Hilbert space. -/
+def radiusRegPowUnboundedOperator (ε s : ℝ) (hε : 0 < ε) :
+    UnboundedOperator (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (hE := schwartzSubmodule_dense) (radiusRegPowOperatorSchwartz ε s)
+    (radiusRegPowOperatorSchwartz_isSymmetric ε s hε)
 
 end
 end QuantumMechanics

PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gregory J. Loges
 -/
 import PhysLean.Mathematics.InnerProductSpace.Submodule
-import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 /-!
 
 # Unbounded operators

PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean

@@ -20,29 +20,45 @@ open MeasureTheory
 open InnerProductSpace
 open SchwartzMap
 
-/-- The continuous linear map including Schwartz functions into `SpaceDHilbertSpace d`. -/
-def schwartzIncl {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2
-
-lemma schwartzIncl_injective {d : ℕ} : Function.Injective (schwartzIncl (d := d)) :=
-  injective_toLp (E := Space d) 2
+variable {d : ℕ}
 
-lemma schwartzIncl_coe_ae {d : ℕ} (f : 𝓢(Space d, ℂ)) : f.1 =ᵐ[volume] (schwartzIncl f) :=
-  (coeFn_toLp f 2).symm
-
-lemma schwartzIncl_inner {d : ℕ} (f g : 𝓢(Space d, ℂ)) :
-    ⟪schwartzIncl f, schwartzIncl g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by
-  apply integral_congr_ae
-  filter_upwards [schwartzIncl_coe_ae f, schwartzIncl_coe_ae g] with _ hf hg
-  rw [← hf, ← hg, RCLike.inner_apply, mul_comm]
-  rfl
+/-- The continuous linear map including Schwartz functions into `SpaceDHilbertSpace d`. -/
+def schwartzIncl : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2
 
 /-- The submodule of `SpaceDHilbertSpace d` consisting of Schwartz functions. -/
 abbrev schwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range
 
-lemma schwartzSubmodule_dense {d : ℕ} :
+instance : CoeFun (schwartzSubmodule d) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩
+
+@[simp]
+lemma val_eq_coe (ψ : schwartzSubmodule d) (x : Space d) : ψ.val x = ψ x := rfl
+
+lemma schwartzSubmodule_dense :
     Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) :=
   denseRange_toLpCLM ENNReal.top_ne_ofNat.symm
 
+/-- The linear equivalence between the Schwartz functions `𝓢(Space d, ℂ)`
+  and the Schwartz submodule of `SpaceDHilbertSpace d`. -/
+def schwartzEquiv : 𝓢(Space d, ℂ) ≃ₗ[ℂ] schwartzSubmodule d :=
+  LinearEquiv.ofInjective schwartzIncl.toLinearMap (injective_toLp (E := Space d) 2)
+
+variable (f g : 𝓢(Space d, ℂ))
+
+lemma schwartzEquiv_coe_ae : (schwartzEquiv f) =ᵐ[volume] f := coeFn_toLp f 2 volume
+
+lemma schwartzEquiv_inner :
+    ⟪schwartzEquiv f, schwartzEquiv g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by
+  apply integral_congr_ae
+  filter_upwards [schwartzEquiv_coe_ae f, schwartzEquiv_coe_ae g] with _ hf hg
+  simp [hf, hg, mul_comm]
+
+lemma schwartzEquiv_ae_eq (h : schwartzEquiv f =ᵐ[volume] schwartzEquiv g) : f = g :=
+  (EmbeddingLike.apply_eq_iff_eq _).mp (SetLike.coe_eq_coe.mp (ext_iff.mpr h))
+
+lemma schwartzEquiv_exists (ψ : schwartzSubmodule d) : ∃ f, ψ = schwartzEquiv f := by
+  use schwartzEquiv.symm ψ
+  exact (LinearEquiv.apply_symm_apply _ _).symm
+
 end
 end SpaceDHilbertSpace
 end QuantumMechanics