feat(QuantumMechanics): add Canonical commutation on the Schwartz submodule

Physlib.lean

@@ -241,14 +241,17 @@ public import Physlib.QuantumMechanics.DDimensions.Basic
 public import Physlib.QuantumMechanics.DDimensions.Hydrogen.Basic
 public import Physlib.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector
 public import Physlib.QuantumMechanics.DDimensions.Operators.AngularMomentum
+public import Physlib.QuantumMechanics.DDimensions.Operators.CanonicalCommutation
 public import Physlib.QuantumMechanics.DDimensions.Operators.Commutation
 public import Physlib.QuantumMechanics.DDimensions.Operators.Momentum
 public import Physlib.QuantumMechanics.DDimensions.Operators.Multiplication
 public import Physlib.QuantumMechanics.DDimensions.Operators.Position
+public import Physlib.QuantumMechanics.DDimensions.Operators.StateCovariance
 public import Physlib.QuantumMechanics.DDimensions.Operators.StateObservables.ExpectedValue
 public import Physlib.QuantumMechanics.DDimensions.Operators.StateObservables.IsEigenvector
 public import Physlib.QuantumMechanics.DDimensions.Operators.StateObservables.Variance
 public import Physlib.QuantumMechanics.DDimensions.Operators.Unbounded
+public import Physlib.QuantumMechanics.DDimensions.Operators.Uncertainty
 public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
 public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.PolyBddSchwartzSubmodule
 public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule

Physlib/Cosmology/FLRW/Basic.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
 public import Physlib.Meta.Linters.Sorry
-public import Physlib.Meta.Informal.Basic
 public import Physlib.SpaceAndTime.Time.Derivatives
 /-!
 

Physlib/QuantumMechanics/DDimensions/Operators/CanonicalCommutation.lean

@@ -0,0 +1,190 @@
+/-
+Copyright (c) 2026 Axiomatic-AI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matteo Cipollina, Austin Letson
+-/
+module
+
+public import Physlib.QuantumMechanics.DDimensions.Operators.Commutation
+public import Physlib.QuantumMechanics.DDimensions.Operators.Momentum
+public import Physlib.QuantumMechanics.DDimensions.Operators.Position
+public import Physlib.QuantumMechanics.DDimensions.Operators.Uncertainty
+/-!
+
+# Canonical commutation on the Schwartz submodule
+
+## i. Overview
+
+In this module we transport the Schwartz canonical commutation relation to
+`schwartzPositionOperator` and `momentumOperator` (`𝓟`) on `schwartzSubmodule d`, and derive the
+same-coordinate uncertainty lower bounds for normalized states.
+
+The operators are defined in `Position` and `Momentum`. The abstract inequalities are proved in
+`Uncertainty` and applied here via `LinearPMap.state_uncertainty_*_of_raw_commutator`.
+
+## ii. Key results
+
+- `schwartzPositionOperator_commutator_momentumOperator` : the transported CCR on
+  `SpaceDHilbertSpace d` as an equality of partial linear maps.
+- `inner_schwartzPositionOperator_commutator_momentumOperator_same` : the same-coordinate
+  commutator expectation for `‖ψ‖ = 1`.
+- `position_momentum_same_coordinate_uncertainty_squared` : the squared Robertson bound.
+- `position_momentum_same_coordinate_uncertainty_squared_with_covariance` : the
+  Robertson–Schrödinger bound.
+- `position_momentum_same_coordinate_uncertainty` : the standard-deviation form.
+
+## iii. Table of contents
+
+- A. Schwartz canonical commutation
+- B. Same-coordinate uncertainty bounds
+
+## iv. References
+
+- [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].
+
+-/
+
+@[expose] public section
+
+namespace QuantumMechanics
+
+open Bracket Complex Constants
+open KroneckerDelta
+open SpaceDHilbertSpace
+open SchwartzSubmodule
+open SchwartzMap
+open InnerProductSpace
+open LinearPMap
+open ContinuousLinearMap
+
+noncomputable section
+
+variable {d : ℕ}
+
+/-!
+
+## A. Schwartz canonical commutation
+
+-/
+
+/-- The momentum operator preserves the domain of the Schwartz-domain position operator. -/
+lemma momentumOperator_mem_schwartzPositionOperator_domain
+    (i j : Fin d) (ψ : (momentumOperator j).domain) :
+    (momentumOperator j ψ : SpaceDHilbertSpace d) ∈ (schwartzPositionOperator i).domain := by
+  rw [schwartzPositionOperator_domain]
+  exact momentumOperator_range j ψ
+
+/-- The Schwartz-domain position operator preserves the domain of the momentum operator. -/
+lemma schwartzPositionOperator_mem_momentumOperator_domain
+    (i j : Fin d) (ψ : (schwartzPositionOperator i).domain) :
+    (schwartzPositionOperator i ψ : SpaceDHilbertSpace d) ∈ (momentumOperator j).domain := by
+  change (schwartzPositionOperator i ψ : SpaceDHilbertSpace d) ∈ schwartzSubmodule d
+  have hψ : (ψ : SpaceDHilbertSpace d) ∈ schwartzSubmodule d := by
+    rw [← schwartzPositionOperator_domain]
+    exact ψ.2
+  exact schwartzPositionOperator_range i ⟨ψ, hψ⟩
+
+/-- Pointwise form of the canonical commutation relation on the Schwartz domain. -/
+lemma schwartzPositionOperator_commutator_momentumOperator_apply (i j : Fin d)
+    (ψ : schwartzSubmodule d) :
+    schwartzPositionOperator i (⟨(momentumOperator j ψ : SpaceDHilbertSpace d),
+          momentumOperator_range j ψ⟩ : schwartzSubmodule d) -
+      momentumOperator j
+        ⟨(schwartzPositionOperator i ψ : SpaceDHilbertSpace d),
+          schwartzPositionOperator_range i ψ⟩ =
+      (I * ℏ) • δ[i,j] • (ψ : SpaceDHilbertSpace d) := by
+  have hψ := congrArg
+    (fun F : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) => F (schwartzEquiv.symm ψ))
+    (position_commutation_momentum i j)
+  simpa [schwartzPositionOperator_apply, momentumOperator_apply, schwartzEquiv.apply_symm_apply,
+    Bracket.bracket, ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply,
+    ContinuousLinearMap.id_apply, Submodule.coe_smul, Submodule.coe_sub] using
+    congrArg Subtype.val (congrArg schwartzEquiv hψ)
+
+/-- The canonical commutation relation for `schwartzPositionOperator` and `momentumOperator` as an
+equality of partial linear maps on the Schwartz domain. -/
+lemma schwartzPositionOperator_commutator_momentumOperator (i j : Fin d) :
+    (schwartzPositionOperator i).comp (momentumOperator j)
+        (momentumOperator_mem_schwartzPositionOperator_domain i j) -
+      (momentumOperator j).comp (schwartzPositionOperator i)
+        (schwartzPositionOperator_mem_momentumOperator_domain i j) =
+      (I * ℏ * (δ[i,j] : ℂ)) •
+        (LinearMap.id.toPMap (schwartzSubmodule d) :
+          SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d) := by
+  apply LinearPMap.ext
+  · rw [LinearPMap.sub_domain, LinearPMap.smul_domain]
+    simp [momentumOperator, schwartzPositionOperator_domain]
+  · intro x hx hy
+    rw [LinearPMap.sub_domain] at hx
+    have hxS : x ∈ schwartzSubmodule d := by
+      simpa [momentumOperator] using hx.1
+    let ψ : schwartzSubmodule d := ⟨x, hxS⟩
+    have hpoint := schwartzPositionOperator_commutator_momentumOperator_apply i j ψ
+    simp [ψ, LinearPMap.sub_apply] at hpoint ⊢
+    rw [← Nat.cast_smul_eq_nsmul ℂ δ[i,j] (x : SpaceDHilbertSpace d), smul_smul] at hpoint
+    simpa [mul_assoc] using hpoint
+
+/-- Expectation-level form of the same-coordinate canonical commutation relation. -/
+lemma inner_schwartzPositionOperator_commutator_momentumOperator_same
+    (i : Fin d) (ψ : schwartzSubmodule d) (hψ_norm : ‖(ψ : SpaceDHilbertSpace d)‖ = 1) :
+    ⟪(ψ : SpaceDHilbertSpace d), (schwartzPositionOperator i
+        (⟨(momentumOperator i ψ : SpaceDHilbertSpace d),
+          momentumOperator_range i ψ⟩ : schwartzSubmodule d) -
+      momentumOperator i
+        ⟨(schwartzPositionOperator i ψ : SpaceDHilbertSpace d),
+          schwartzPositionOperator_range i ψ⟩)⟫_ℂ =
+      I * ℏ := by
+  rw [schwartzPositionOperator_commutator_momentumOperator_apply i i ψ]
+  simp only [KroneckerDelta.eq_one_of_same, one_smul]
+  rw [inner_smul_right, inner_self_eq_norm_sq_to_K, hψ_norm, sq]
+  simp
+
+/-!
+
+## B. Same-coordinate uncertainty bounds
+
+-/
+
+/-- The same-coordinate position and momentum variances satisfy the squared Heisenberg lower bound
+on normalized Schwartz-domain states. -/
+lemma position_momentum_same_coordinate_uncertainty_squared
+    (i : Fin d) (ψ : schwartzSubmodule d) (hψ_norm : ‖(ψ : SpaceDHilbertSpace d)‖ = 1) :
+    (ℏ / 2) ^ 2 ≤ variance (schwartzPositionOperator i) ψ *
+      variance (momentumOperator i) ⟨ψ, ψ.2⟩ := by
+  have hbound :=
+    state_uncertainty_squared_of_raw_commutator (schwartzPositionOperator i) (momentumOperator i)
+      (schwartzPositionOperator_isSymmetric i) (momentumOperator_isSymmetric i) ψ ψ.2 hψ_norm
+      (schwartzPositionOperator_range i ψ)
+      (momentumOperator_mem_schwartzPositionOperator_domain i i ψ) (c := ℏ)
+      (inner_schwartzPositionOperator_commutator_momentumOperator_same i ψ hψ_norm)
+  simpa only [abs_of_nonneg ℏ_nonneg] using hbound
+
+/-- The same-coordinate Robertson–Schrödinger lower bound on normalized Schwartz-domain states. -/
+lemma position_momentum_same_coordinate_uncertainty_squared_with_covariance
+    (i : Fin d) (ψ : schwartzSubmodule d) (hψ_norm : ‖(ψ : SpaceDHilbertSpace d)‖ = 1) :
+    (stateCovariance (schwartzPositionOperator i) (momentumOperator i) ψ ψ.2) ^ 2 +
+        (ℏ / 2) ^ 2 ≤
+      variance (schwartzPositionOperator i) ψ *
+        variance (momentumOperator i) ⟨ψ, ψ.2⟩ := by
+  exact state_uncertainty_squared_with_covariance_of_raw_commutator (schwartzPositionOperator i)
+    (momentumOperator i) (schwartzPositionOperator_isSymmetric i)
+    (momentumOperator_isSymmetric i) ψ ψ.2 hψ_norm (schwartzPositionOperator_range i ψ)
+    (momentumOperator_mem_schwartzPositionOperator_domain i i ψ) (c := ℏ)
+    (inner_schwartzPositionOperator_commutator_momentumOperator_same i ψ hψ_norm)
+
+/-- The same-coordinate position and momentum standard deviations satisfy the Heisenberg lower
+bound on normalized Schwartz-domain states. -/
+lemma position_momentum_same_coordinate_uncertainty
+    (i : Fin d) (ψ : schwartzSubmodule d) (hψ_norm : ‖(ψ : SpaceDHilbertSpace d)‖ = 1) :
+    ℏ / 2 ≤ standardDeviation (schwartzPositionOperator i) ψ *
+      standardDeviation (momentumOperator i) ⟨ψ, ψ.2⟩ := by
+  have hbound :=
+    state_uncertainty_of_raw_commutator (schwartzPositionOperator i) (momentumOperator i)
+      (schwartzPositionOperator_isSymmetric i) (momentumOperator_isSymmetric i) ψ ψ.2 hψ_norm
+      (schwartzPositionOperator_range i ψ)
+      (momentumOperator_mem_schwartzPositionOperator_domain i i ψ) (c := ℏ)
+      (inner_schwartzPositionOperator_commutator_momentumOperator_same i ψ hψ_norm)
+  simpa only [abs_of_nonneg ℏ_nonneg] using hbound
+
+end
+end QuantumMechanics

Physlib/QuantumMechanics/DDimensions/Operators/Position.lean

@@ -6,6 +6,7 @@ Authors: Gregory J. Loges
 module
 
 public import Physlib.QuantumMechanics.DDimensions.Operators.Multiplication
+public import Physlib.QuantumMechanics.DDimensions.Operators.Unbounded
 public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.PolyBddSchwartzSubmodule
 public import Physlib.SpaceAndTime.Space.Integrals.NormPow
 public import Physlib.SpaceAndTime.Space.Derivatives.Basic
@@ -25,7 +26,9 @@ Definitions:
 - `radiusRegPowCLM` : operator acting on Schwartz maps by multiplication by
     `(‖x‖² + ε²)^(s/2)`, a smooth regularization of `‖x‖ˢ`.
 - `positionOperator` : a self-adjoint multiplication operator acting on `SpaceDHilbertSpace d`.
-- `readiusRegPowOperator` : a self-adjoint multiplication operator acting on `SpaceDHilbertSpace d`.
+- `schwartzPositionOperator` : the position operator restricted to the Schwartz submodule of
+    `SpaceDHilbertSpace d`.
+- `radiusRegPowOperator` : a self-adjoint multiplication operator acting on `SpaceDHilbertSpace d`.
 
 Notation:
 - `𝐱` for `positionCLM`
@@ -41,9 +44,10 @@ Notation:
     - A.3.1. As limit of regularized operators
 - B. Unbounded operators
   - B.1. Position vector
-  - B.2. Radius powers (regularized)
-  - B.3. Radius powers
-    - B.3.1. As limit of regularized operators
+  - B.2. Schwartz-domain position
+  - B.3. Radius powers (regularized)
+  - B.4. Radius powers
+    - B.4.1. As limit of regularized operators
 
 ## iv. References
 
@@ -403,8 +407,88 @@ lemma positionOperator_isSelfAdjoint : IsSelfAdjoint (𝓧 i) :=
 lemma positionOperator_isUnbounded : (𝓧 i).IsUnbounded :=
   LinearPMap.IsSelfAdjoint.isUnbounded (positionOperator_isSelfAdjoint i)
 
+lemma schwartzSubmodule_le_positionOperator_domain :
+    schwartzSubmodule d ≤ (𝓧 i).domain := by
+  simpa [positionOperator] using
+    SpaceDHilbertSpace.mulOperator_domain_ge_of_hasTemperateGrowth
+      (d := d) (f := Complex.ofRealCLM ∘L Space.coordCLM i) (by fun_prop)
+
+/-!
+### B.2. Schwartz-domain position
+-/
+
+/-- The position operator restricted to the Schwartz submodule. -/
+def schwartzPositionOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d :=
+  (𝓧 i).domRestrict (schwartzSubmodule d)
+
+@[simp]
+lemma schwartzPositionOperator_domain :
+    (schwartzPositionOperator i).domain = schwartzSubmodule d := by
+  rw [schwartzPositionOperator, LinearPMap.domRestrict_domain, inf_eq_left]
+  exact schwartzSubmodule_le_positionOperator_domain i
+
+/-- Regard a Schwartz-domain vector as an element of the domain of `schwartzPositionOperator`. -/
+abbrev schwartzPositionOperatorDomain (ψ : schwartzSubmodule d) :
+    (schwartzPositionOperator i).domain :=
+  ⟨ψ, by rw [schwartzPositionOperator_domain]; exact ψ.2⟩
+
+/-- Coerce a Schwartz-domain vector into the domain of the restricted position operator. -/
+instance : Coe (schwartzSubmodule d) (schwartzPositionOperator i).domain where
+  coe := schwartzPositionOperatorDomain i
+
+@[simp]
+lemma schwartzPositionOperator_apply (ψ : schwartzSubmodule d) :
+    schwartzPositionOperator i ψ = schwartzEquiv (𝐱 i (schwartzEquiv.symm ψ)) := by
+  obtain ⟨f, rfl⟩ := schwartzEquiv.surjective ψ
+  rw [schwartzEquiv.symm_apply_apply]
+  change ((𝓧 i).domRestrict (schwartzSubmodule d))
+      ⟨schwartzEquiv f, ⟨(schwartzEquiv f).2,
+        schwartzSubmodule_le_positionOperator_domain i (schwartzEquiv f).2⟩⟩ =
+    schwartzEquiv (𝐱 i f)
+  have hrestrict :
+      ((𝓧 i).domRestrict (schwartzSubmodule d))
+          ⟨schwartzEquiv f, ⟨(schwartzEquiv f).2,
+            schwartzSubmodule_le_positionOperator_domain i (schwartzEquiv f).2⟩⟩ =
+        (𝓧 i) ⟨schwartzEquiv f,
+          schwartzSubmodule_le_positionOperator_domain i (schwartzEquiv f).2⟩ :=
+    LinearPMap.domRestrict_apply rfl
+  rw [hrestrict]
+  apply SpaceDHilbertSpace.ext_iff.mpr
+  filter_upwards [mulOperator_apply_ae ⟨schwartzEquiv f,
+    schwartzSubmodule_le_positionOperator_domain i (schwartzEquiv f).2⟩,
+    schwartzEquiv_coe_ae f, schwartzEquiv_coe_ae (𝐱 i f)] with x h𝓧 hf hx
+  change (((𝓜 ⇑(Complex.ofRealCLM.comp (Space.coordCLM i))) ⟨schwartzEquiv f, _⟩ :
+    SpaceDHilbertSpace d) : Space d → ℂ) x =
+      ((schwartzEquiv ((𝐱 i) f) : SpaceDHilbertSpace d) : Space d → ℂ) x
+  rw [h𝓧, hx]
+  simp [hf, Space.coordCLM_apply, Space.coord_apply, positionCLM_apply]
+
+lemma schwartzPositionOperator_range (ψ : schwartzSubmodule d) :
+    schwartzPositionOperator i ψ ∈ schwartzSubmodule d := by
+  simp [schwartzPositionOperator_apply]
+
+lemma schwartzPositionOperator_hasDenseDomain :
+    (schwartzPositionOperator i).HasDenseDomain := by
+  rw [LinearPMap.hasDenseDomain_def, schwartzPositionOperator_domain]
+  exact SchwartzSubmodule.dense d
+
+lemma schwartzPositionOperator_le_positionOperator :
+    schwartzPositionOperator i ≤ 𝓧 i :=
+  LinearPMap.domRestrict_le
+
+lemma schwartzPositionOperator_isSymmetric :
+    (schwartzPositionOperator i).IsSymmetric :=
+  (LinearPMap.IsSelfAdjoint.isSymmetric (positionOperator_isSelfAdjoint i)).of_le
+    (schwartzPositionOperator_le_positionOperator i)
+
+lemma schwartzPositionOperator_isUnbounded :
+    (schwartzPositionOperator i).IsUnbounded := by
+  refine (LinearPMap.IsSymmetric.isUnbounded_iff_hasDenseDomain ?_).mpr ?_
+  · exact schwartzPositionOperator_isSymmetric i
+  · exact schwartzPositionOperator_hasDenseDomain i
+
 /-!
-### B.2. Radius powers (regularized)
+### B.3. Radius powers (regularized)
 -/
 
 /-- The operator on `SpaceDHilbertSpace d` acting by multiplication by
@@ -428,7 +512,7 @@ lemma radiusRegPowOperator_isUnbounded (ε : ℝˣ) (s : ℝ) : (𝓡₀[d] ε s
   LinearPMap.IsSelfAdjoint.isUnbounded (radiusRegPowOperator_isSelfAdjoint ε s)
 
 /-!
-### B.3. Radius powers
+### B.4. Radius powers
 -/
 
 /-- The operator on `SpaceDHilbertSpace d` acting by multiplication by `fun x ↦ ‖x‖ˢ`. -/