feat: Unbounded operators from H1 to H2

PhysLean/Mathematics/InnerProductSpace/Submodule.lean

@@ -6,12 +6,12 @@ Authors: Gregory J. Loges
 import Mathlib.Analysis.InnerProductSpace.LinearPMap
 /-!
 
-# Submodules of `E × E`
+# Submodules of `E × F`
 
-In this module we define `submoduleToLp` which reinterprets a submodule of `E × E`,
-where `E` is an inner product space, as a submodule of `WithLp 2 (E × E)`.
+In this module we define `submoduleToLp` which reinterprets a submodule of `E × F`,
+where `E` and `F` are inner product spaces, as a submodule of `WithLp 2 (E × F)`.
 This allows us to take advantage of the inner product structure, since otherwise
-by default `E × E` is given the sup norm.
+by default `E × F` is given the sup norm.
 
 -/
 
@@ -21,10 +21,12 @@ open LinearPMap Submodule
 
 variable
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
-  (M : Submodule ℂ (E × E))
+  {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
+  (M : Submodule ℂ (E × F))
+  (f : E × F) (g : F × E)
 
-/-- The submodule of `WithLp 2 (E × E)` defined by `M`. -/
-def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where
+/-- The submodule of `WithLp 2 (E × F)` defined by `M`. -/
+def submoduleToLp : Submodule ℂ (WithLp 2 (E × F)) where
   carrier := {x | x.ofLp ∈ M}
   add_mem' := by
     intro a b ha hb
@@ -34,8 +36,8 @@ def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where
     intro c x hx
     exact Submodule.smul_mem M c hx
 
-lemma mem_submodule_iff_mem_submoduleToLp (f : E × E) :
-    f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M := Eq.to_iff rfl
+lemma mem_submodule_iff_mem_submoduleToLp : f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M :=
+  Eq.to_iff rfl
 
 lemma submoduleToLp_closure :
     (submoduleToLp M.topologicalClosure) = (submoduleToLp M).topologicalClosure := by
@@ -67,31 +69,31 @@ lemma submoduleToLp_closure :
     use w.ofLp
     exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp M)).mp hw.2⟩
 
-lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (f : E × E) :
+lemma mem_submodule_closure_iff_mem_submoduleToLp_closure :
     f ∈ M.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp M).topologicalClosure := by
   rw [← submoduleToLp_closure]
   rfl
 
-lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal (f : E × E) :
-    f ∈ M.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M)ᗮ := by
+lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal :
+    g ∈ M.adjoint ↔ WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M)ᗮ := by
   constructor <;> intro h
   · rw [mem_orthogonal]
     intro u hu
     rw [mem_adjoint_iff] at h
-    have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by
+    have h' : inner ℂ u.snd g.1 = inner ℂ u.fst g.2 := by
       rw [← sub_eq_zero]
       exact h u.fst u.snd hu
     simp [h']
   · rw [mem_adjoint_iff]
     intro a b hab
     rw [mem_orthogonal] at h
     have hab' := (mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab
-    have h' : inner ℂ a f.2 = inner ℂ b f.1 := by
+    have h' : inner ℂ a g.2 = inner ℂ b g.1 := by
       rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right]
       exact h (WithLp.toLp 2 (a, b)) hab'
     simp [h']
 
-lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal (f : E × E) :
+lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal :
     f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ := by
   simp only [mem_adjoint_iff]
   trans ∀ v, (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0
@@ -112,9 +114,9 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal
       simp [hw']
   simp only [← mem_orthogonal]
 
-lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E) :
-    f ∈ M.topologicalClosure.adjoint ↔
-    WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).topologicalClosureᗮ := by
+lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal :
+    g ∈ M.topologicalClosure.adjoint ↔
+    WithLp.toLp 2 (g.2, -g.1) ∈ (submoduleToLp M).topologicalClosureᗮ := by
   rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal, submoduleToLp_closure]
 
 end InnerProductSpaceSubmodule

PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean

@@ -116,8 +116,8 @@ lemma momentumOperatorSchwartz_isSymmetric : (momentumOperatorSchwartz i).IsSymm
 /-- 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 d) (momentumOperatorSchwartz i)
+def momentumUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d) (momentumOperatorSchwartz i)
     (momentumOperatorSchwartz_isSymmetric i)
 
 end

PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean

@@ -184,8 +184,8 @@ lemma positionOperatorSchwartz_isSymmetric : (positionOperatorSchwartz i).IsSymm
 
 /-- The symmetric position unbounded operators with domain the Schwartz submodule
   of the Hilbert space. -/
-def positionUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (hE := schwartzSubmodule_dense d) (positionOperatorSchwartz i)
+def positionUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d) (positionOperatorSchwartz i)
     (positionOperatorSchwartz_isSymmetric i)
 
 /-!
@@ -213,8 +213,8 @@ lemma radiusRegPowOperatorSchwartz_isSymmetric (ε s : ℝ) (hε : 0 < ε) :
 /-- 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 d) (radiusRegPowOperatorSchwartz ε s)
+    UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d) (radiusRegPowOperatorSchwartz ε s)
     (radiusRegPowOperatorSchwartz_isSymmetric ε s hε)
 
 end

PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean

@@ -21,6 +21,8 @@ We prove some basic relations, making use of the density and closability assumpt
 
 ## References
 
+- M. Reed & B. Simon, (1972). "Methods of modern mathematical physics: Vol. 1. Functional analysis".
+  Academic Press. https://doi.org/10.1016/B978-0-12-585001-8.X5001-6
 - K. Schmüdgen, (2012). "Unbounded self-adjoint operators on Hilbert space" (Vol. 265). Springer.
   https://doi.org/10.1007/978-94-007-4753-1
 
@@ -29,30 +31,32 @@ We prove some basic relations, making use of the density and closability assumpt
 namespace QuantumMechanics
 
 open LinearPMap Submodule
+open InnerProductSpaceSubmodule
 
-/-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space
-  to the Hilbert space, assumed to be both densely defined and closable. -/
+/-- An `UnboundedOperator` is a linear map from a submodule of `H` to `H'`,
+  assumed to be both densely defined and closable. -/
 @[ext]
 structure UnboundedOperator
-    (HS : Type*) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS]
-    extends LinearPMap ℂ HS HS where
-  /-- The domain of an unbounded operator is dense in the Hilbert space. -/
-  dense_domain : Dense (domain : Set HS)
+    (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    (H' : Type*) [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H']
+    extends LinearPMap ℂ H H' where
+  /-- The domain of an unbounded operator is dense in `H`. -/
+  dense_domain : Dense (domain : Set H)
   /-- An unbounded operator is closable. -/
   is_closable : toLinearPMap.IsClosable
 
 namespace UnboundedOperator
 
 variable
-  {HS : Type*} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS]
-  (U : UnboundedOperator HS)
+  {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+  {H' : Type*} [NormedAddCommGroup H'] [InnerProductSpace ℂ H'] [CompleteSpace H']
 
-lemma ext' (U T : UnboundedOperator HS) (h : U.toLinearPMap = T.toLinearPMap) : U = T := by
+lemma ext' (U T : UnboundedOperator H H') (h : U.toLinearPMap = T.toLinearPMap) : U = T := by
   apply UnboundedOperator.ext
   · exact toSubMulAction_inj.mp (congrArg toSubMulAction (congrArg domain h))
   · exact congr_arg_heq toFun h
 
-lemma ext_iff' (U T : UnboundedOperator HS) : U = T ↔ U.toLinearPMap = T.toLinearPMap := by
+lemma ext_iff' (U T : UnboundedOperator H H') : U = T ↔ U.toLinearPMap = T.toLinearPMap := by
   refine ⟨?_, UnboundedOperator.ext' U T⟩
   intro h
   rw [h]
@@ -61,10 +65,12 @@ lemma ext_iff' (U T : UnboundedOperator HS) : U = T ↔ U.toLinearPMap = T.toLin
 ### Construction of unbounded operators
 -/
 
-variable {E : Submodule ℂ HS} {hE : Dense (E : Set HS)}
+section
+
+variable {E : Submodule ℂ H} (hE : Dense (E : Set H))
 
 /-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/
-def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator HS where
+def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H H where
   toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f)
   dense_domain := hE
   is_closable := by
@@ -74,16 +80,20 @@ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H
 
 @[simp]
 lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) :
-    (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl
+    (ofSymmetric hE f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl
+
+end
 
 /-!
 ### Closure
 -/
 
 section Closure
 
+variable (U : UnboundedOperator H H')
+
 /-- The closure of an unbounded operator. -/
-noncomputable def closure : UnboundedOperator HS where
+noncomputable def closure : UnboundedOperator H H' where
   toLinearPMap := U.toLinearPMap.closure
   dense_domain := Dense.mono (HasCore.le_domain (closureHasCore U.toLinearPMap)) U.dense_domain
   is_closable := IsClosed.isClosable (IsClosable.closure_isClosed U.is_closable)
@@ -104,11 +114,11 @@ end Closure
 
 section Adjoints
 
-open InnerProductSpaceSubmodule
+variable (U : UnboundedOperator H H')
 
 /-- The adjoint of a densely defined, closable `LinearPMap` is densely defined. -/
-lemma adjoint_isClosable_dense (f : LinearPMap ℂ HS HS) (h_dense : Dense (f.domain : Set HS))
-    (h_closable : f.IsClosable) : Dense (f†.domain : Set HS) := by
+lemma adjoint_isClosable_dense (f : LinearPMap ℂ H H') (h_dense : Dense (f.domain : Set H))
+    (h_closable : f.IsClosable) : Dense (f†.domain : Set H') := by
   by_contra hd
   have : ∃ x ∈ f†.domainᗮ, x ≠ 0 := by
     apply not_forall.mp at hd
@@ -135,26 +145,17 @@ lemma adjoint_isClosable_dense (f : LinearPMap ℂ HS HS) (h_dense : Dense (f.do
   exact hx y (mem_domain_of_mem_graph hy)
 
 /-- The adjoint of an unbounded operator, denoted as `U†`. -/
-noncomputable def adjoint : UnboundedOperator HS where
+noncomputable def adjoint : UnboundedOperator H' H where
   toLinearPMap := U.toLinearPMap.adjoint
   dense_domain := adjoint_isClosable_dense U.toLinearPMap U.dense_domain U.is_closable
   is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain)
 
 @[inherit_doc]
 scoped postfix:1024 "†" => UnboundedOperator.adjoint
 
-noncomputable instance instStar : Star (UnboundedOperator HS) where
-  star := fun U ↦ U.adjoint
-
 @[simp]
 lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl
 
-lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl
-
-lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by
-  rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap,
-    UnboundedOperator.ext_iff']
-
 lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain
 
 lemma closure_adjoint_eq_adjoint : U.closure† = U† := by
@@ -181,18 +182,43 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by
 
 end Adjoints
 
+/-!
+### Self-adjoint
+-/
+
+section
+
+variable (U : UnboundedOperator H H)
+
+noncomputable instance instStar : Star (UnboundedOperator H H) where
+  star := fun U ↦ U.adjoint
+
+lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl
+
+lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by
+  rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap,
+    UnboundedOperator.ext_iff']
+
+end
+
 /-!
 ### Generalized eigenvectors
 -/
 
+section
+
+variable
+  {E : Submodule ℂ H} (hE : Dense (E : Set H))
+  (U : UnboundedOperator H H)
+
 /-- A map `F : D(U) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `U`
   if there is an eigenvalue `c` such that for all `ψ ∈ D(U)`, `F (U ψ) = c ⬝ F ψ`. -/
 def IsGeneralizedEigenvector (F : U.domain →L[ℂ] ℂ) (c : ℂ) : Prop :=
   ∀ ψ : U.domain, ∃ ψ' : U.domain, ψ' = U.toFun ψ ∧ F ψ' = c • F ψ
 
 lemma isGeneralizedEigenvector_ofSymmetric_iff
     {f : E →ₗ[ℂ] E} (hf : f.IsSymmetric) (F : E →L[ℂ] ℂ) (c : ℂ) :
-    IsGeneralizedEigenvector (ofSymmetric (hE := hE) f hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by
+    IsGeneralizedEigenvector (ofSymmetric hE f hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by
   constructor <;> intro h ψ
   · obtain ⟨ψ', hψ', hψ''⟩ := h ψ
     apply SetLike.coe_eq_coe.mp at hψ'
@@ -201,5 +227,7 @@ lemma isGeneralizedEigenvector_ofSymmetric_iff
   · use f ψ
     exact ⟨by simp, h ψ⟩
 
+end
+
 end UnboundedOperator
 end QuantumMechanics