feat: Initial progress with d-dimensional QM operators

PhysLean.lean

@@ -225,6 +225,10 @@ import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
 import PhysLean.QFT.QED.AnomalyCancellation.Permutations
 import PhysLean.QFT.QED.AnomalyCancellation.Sorts
 import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
+import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Position
 import PhysLean.QuantumMechanics.FiniteTarget.Basic
 import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
 import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic

PhysLean/QuantumMechanics/DDimensions/Operators/AngularMomentum.lean

@@ -0,0 +1,120 @@
+/-
+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.Position
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+/-!
+
+# Angular momentum operator
+
+In this module we define:
+- The angular momentum operator on Schwartz maps, component-wise.
+- The angular momentum squared operator.
+- The angular momentum scalar operator in 2d and angular momentum vector operator in 3d.
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open ContDiff SchwartzMap
+
+/-
+
+# Definition
+
+-/
+
+/-- Component `i j` of the angular momentum operator is the continuous linear map
+from `𝓢(Space d, ℂ)` to itself defined by `𝐋ᵢⱼ ≔ 𝐱ᵢ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᵢ`. -/
+@[sorryful]
+def angularMomentumOperator {d : ℕ} (i j : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  𝐱[i] ∘L 𝐩[j] - 𝐱[j] ∘L 𝐩[i]
+
+@[inherit_doc angularMomentumOperator]
+macro "𝐋[" i:term "," j:term "]" : term => `(angularMomentumOperator $i $j)
+
+@[sorryful]
+lemma angularMomentumOperator_apply_fun {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+    𝐋[i,j] ψ = 𝐱[i] (𝐩[j] ψ) - 𝐱[j] (𝐩[i] ψ) := rfl
+
+@[sorryful]
+lemma angularMomentumOperator_apply {d : ℕ} (i j : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐋[i,j] ψ x = 𝐱[i] (𝐩[j] ψ) x - 𝐱[j] (𝐩[i] ψ) x := rfl
+
+/-- The square of the angular momentum operator, `𝐋² ≔ ½ ∑ᵢⱼ 𝐋ᵢⱼ∘𝐋ᵢⱼ`. -/
+@[sorryful]
+def angularMomentumOperatorSqr {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
+  ∑ i, ∑ j, (2 : ℂ)⁻¹ • 𝐋[i,j] ∘L 𝐋[i,j]
+
+@[inherit_doc angularMomentumOperatorSqr]
+notation "𝐋²" => angularMomentumOperatorSqr
+
+@[sorryful]
+lemma angularMomentumOperatorSqr_apply_fun {d : ℕ} (ψ : 𝓢(Space d, ℂ)) :
+    𝐋² ψ = ∑ i, ∑ j, (2 : ℂ)⁻¹ • 𝐋[i,j] (𝐋[i,j] ψ) := by
+  dsimp only [angularMomentumOperatorSqr]
+  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_smul',
+    ContinuousLinearMap.coe_comp', Finset.sum_apply, Pi.smul_apply, Function.comp_apply]
+
+@[sorryful]
+lemma angularMomentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
+    𝐋² ψ x = ∑ i, ∑ j, (2 : ℂ)⁻¹ * 𝐋[i,j] (𝐋[i,j] ψ) x := by
+  rw [angularMomentumOperatorSqr_apply_fun]
+  rw [← SchwartzMap.coe_coeHom]
+  simp only [map_sum, Finset.sum_apply]
+  rfl
+
+/-
+
+## Basic properties
+
+-/
+
+/-- The angular momentum operator is antisymmetric, `𝐋ᵢⱼ = -𝐋ⱼᵢ` -/
+@[sorryful]
+lemma angularMomentumOperator_antisymm {d : ℕ} (i j : Fin d) : 𝐋[i,j] = - 𝐋[j,i] :=
+  Eq.symm (neg_sub _ _)
+
+/-- Angular momentum operator components with repeated index vanish, `𝐋ᵢᵢ = 0`. -/
+@[sorryful]
+lemma angularMomentumOperator_eq_zero {d : ℕ} (i : Fin d) : 𝐋[i,i] = 0 := sub_self _
+
+/-
+
+## Special cases in low dimensions
+
+  • d = 1 : The angular momentum operator is trivial.
+
+  • d = 2 : The angular momentum operator has only one independent component, 𝐋₀₁, which may
+            be thought of as a (pseudo)scalar operator.
+
+  • d = 3 : The angular momentum operator has three independent components, 𝐋₀₁, 𝐋₁₂ and 𝐋₂₀.
+            Dualizing using the Levi-Civita symbol produces the familiar (pseudo)vector angular
+            momentum operator with components 𝐋₀ = 𝐋₂₀, 𝐋₁ = 𝐋₂₀ and 𝐋₂ = 𝐋₀₁.
+
+-/
+
+/-- In one dimension the angular momentum operator is trivial. -/
+@[sorryful]
+lemma angularMomentumOperator1D_trivial : ∀ (i j : Fin 1), 𝐋[i,j] = 0 := by
+  intro i j
+  fin_cases i, j
+  exact angularMomentumOperator_eq_zero 0
+
+/-- The angular momentum (pseudo)scalar operator in two dimensions, `𝐋 ≔ 𝐋₀₁`. -/
+@[sorryful]
+def angularMomentumOperator2D : 𝓢(Space 2, ℂ) →L[ℂ] 𝓢(Space 2, ℂ) := 𝐋[0,1]
+
+/-- The angular momentum (pseudo)vector operator in three dimension, `𝐋ᵢ ≔ ½ ∑ⱼₖ εᵢⱼₖ 𝐋ⱼₖ`. -/
+@[sorryful]
+def angularMomentumOperator3D (i : Fin 3) : 𝓢(Space 3, ℂ) →L[ℂ] 𝓢(Space 3, ℂ) :=
+  match i with
+    | 0 => 𝐋[1,2]
+    | 1 => 𝐋[2,0]
+    | 2 => 𝐋[0,1]
+
+end
+end QuantumMechanics

PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean

@@ -0,0 +1,110 @@
+/-
+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.AngularMomentum
+/-!
+
+# Commutation relations
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open SchwartzMap
+
+/-
+## Position / position commutators
+-/
+
+/-- `[xᵢ, xⱼ] = 0` -/
+@[sorryful]
+lemma position_commutation_position {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐱[j]⁆ = 0 := by
+  dsimp only [Bracket.bracket]
+  ext ψ x
+  simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_mul, Pi.sub_apply, sub_apply,
+    Function.comp_apply, ContinuousLinearMap.zero_apply, zero_apply, positionOperator_apply]
+  ring
+
+/-
+## Momentum / momentum commutators
+-/
+
+/-- `[pᵢ, pⱼ] = 0` -/
+@[sorryful]
+lemma momentum_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐩[i], 𝐩[j]⁆ = 0 := by
+  sorry
+
+@[sorryful]
+lemma momentum_momentum_eq {d : ℕ} (i j : Fin d) : 𝐩[i] ∘L 𝐩[j] = 𝐩[j] ∘L 𝐩[i] := by
+  rw [← sub_eq_zero]
+  exact momentum_commutation_momentum i j
+
+/-- `[𝐩², 𝐩ᵢ] = 0` -/
+@[sorryful]
+lemma momentumSqr_commutation_momentum {d : ℕ} (i : Fin d) : 𝐩² ∘L 𝐩[i] - 𝐩[i] ∘L 𝐩² = 0 := by
+  dsimp only [momentumOperatorSqr]
+  simp only [ContinuousLinearMap.finset_sum_comp, ContinuousLinearMap.comp_finset_sum]
+  rw [sub_eq_zero]
+  congr
+  ext j ψ x
+  rw [ContinuousLinearMap.comp_assoc]
+  rw [momentum_momentum_eq]
+  rw [← ContinuousLinearMap.comp_assoc]
+  rw [momentum_momentum_eq]
+  rfl
+
+/-
+## Position / momentum commutators
+-/
+
+/-- `[xᵢ, pⱼ] = iℏ δᵢⱼ𝟙` -/
+@[sorryful]
+lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j]⁆ =
+    (Complex.I * ℏ) • (if i = j then 1 else 0) • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by
+  sorry
+
+/-
+## Angular momentum / position commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_position {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐱[k]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐱[j] - (if j = k then 1 else 0) * 𝐱[i]) := by
+  sorry
+
+@[sorryful]
+lemma angularMomentumSqr_commutation_position {d : ℕ} (i : Fin d) :
+    𝐋² ∘L 𝐱[i] - 𝐱[i] ∘L 𝐋² = 0 := by
+  sorry
+
+/-
+## Angular momentum / momentum commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐋[i,j], 𝐩[k]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐩[j] - (if j = k then 1 else 0) * 𝐩[i]) := by
+  sorry
+
+/-
+## Angular momentum / angular momentum commutators
+-/
+
+@[sorryful]
+lemma angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : ⁅𝐋[i,j], 𝐋[k,l]⁆ =
+    (Complex.I * ℏ) • ((if i = k then 1 else 0) * 𝐋[j,l]
+                      - (if i = l then 1 else 0) * 𝐋[j,k]
+                      - (if j = k then 1 else 0) * 𝐋[i,l]
+                      + (if j = l then 1 else 0) * 𝐋[i,k]) := by
+  sorry
+
+@[sorryful]
+lemma angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) :
+    𝐋² ∘L 𝐋[i,j] - 𝐋[i,j] ∘L 𝐋² = 0 := by
+  sorry
+
+end
+end QuantumMechanics

PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean

@@ -0,0 +1,52 @@
+/-
+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.PlanckConstant
+/-!
+
+# Momentum vector operator
+
+In this module we define:
+- The momentum operator on Schwartz maps, component-wise.
+- The momentum squared operator on Schwartz maps.
+
+-/
+
+namespace QuantumMechanics
+noncomputable section
+open Constants
+open Space
+open ContDiff SchwartzMap
+
+/-- 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, ℂ) :=
+  (- Complex.I * ℏ) • (SchwartzMap.evalCLM (basis i)) ∘L (SchwartzMap.fderivCLM ℂ)
+
+@[inherit_doc momentumOperator]
+macro "𝐩[" i:term "]" : term => `(momentumOperator $i)
+
+lemma momentumOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) :
+    𝐩[i] ψ = (- Complex.I * ℏ) • ∂[i] ψ := rfl
+
+lemma momentumOperator_apply {d : ℕ} (i : Fin d) (ψ : 𝓢(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]
+
+@[inherit_doc momentumOperatorSqr]
+notation "𝐩²" => momentumOperatorSqr
+
+lemma momentumOperatorSqr_apply {d : ℕ} (ψ : 𝓢(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]
+
+end
+end QuantumMechanics