Skip to content

feat: lift angular momentum to Hilbert space #1673

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jstoobysmith merged 3 commits into from
Sep 22, 2026
+211 −137
Merged

feat: lift angular momentum to Hilbert space #1673

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ac7438e
feat: lift angular momentum to Hilbert space
Sep 22, 2026
1d12dc2
refactor: consolidate angular momentum operators and lemmas
Sep 22, 2026
ff24e7a
Merge upstream/master into angular momentum branch
Sep 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Authors: Gregory J. Loges
module

public import Physlib.QuantumMechanics.Hydrogen.Basic
public import Physlib.QuantumMechanics.Operators.Commutation
public import Physlib.QuantumMechanics.Operators.AngularMomentum
/-!

# Laplace-Runge-Lenz vector
Expand Down Expand Up @@ -48,7 +48,7 @@ lemma lrlOperator_eq (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = 𝐱 i
calc
_ = (2 : ℝ)⁻¹ • ∑ j, ((𝐩 j ∘L 𝐱 i) ∘L 𝐩 j + 𝐱 i ∘L 𝐩 j ∘L 𝐩 j
- ((𝐩 j ∘L 𝐱 j) ∘L 𝐩 i + 𝐱 j ∘L 𝐩 j ∘L 𝐩 i)) := by
simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumOperator, comp_sub,
simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumCLM, comp_sub,
sub_comp, comp_assoc, momentum_comp_commute, ← sub_sub, add_sub, sub_add_eq_add_sub]
_ = (2 : ℂ)⁻¹ • ∑ j, ((2 : ℂ) • 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - (I * ℏ) • δ[i,j] • 𝐩 j
- ((2 : ℂ) • (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i - (I * ℏ) • 𝐩 i)) := by
Expand All @@ -72,7 +72,7 @@ lemma lrlOperator_eq' (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i =
rw [lrlOperator_eq, sub_left_inj, add_left_inj]
symm
trans ∑ j, 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - ∑ j, (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i
· simp [dotProduct, mul_def, angularMomentumOperator, comp_assoc, momentum_comp_commute]
· simp [dotProduct, mul_def, angularMomentumCLM, comp_assoc, momentum_comp_commute]
simp [← comp_finsetSum, ← finsetSum_comp, dotProduct, mul_def]

/-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
Expand Down Expand Up @@ -103,7 +103,7 @@ lemma angularMomentum_commutation_Ldot_p (i j k : Fin H.d) :
comp_smul, smul_comp, comp_sub, sub_comp, add_comp]
simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum,
KroneckerDelta.sum_smul]
rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j]
rw [angularMomentumCLM_antisymm k i, angularMomentumCLM_antisymm k j]
simp only [neg_comp]
module

Expand Down Expand Up @@ -182,9 +182,9 @@ private lemma positionCompMomentumSqr_comm {d : ℕ} (i j : Fin d) :
simp [lie_leibniz, leibniz_lie, comp_assoc]
_ = (2 * I * ℏ) • 𝐋 j i ∘L (𝐩 ⬝ᵥ 𝐩) := by
simp_rw [← lie_skew (𝐩 ⬝ᵥ 𝐩) _, position_commutation_momentumSqr, comp_neg, comp_smul,
← sub_eq_add_neg, ← smul_sub, smul_comp, angularMomentumOperator]
← sub_eq_add_neg, ← smul_sub, smul_comp, angularMomentumCLM]
_ = (-2 * I * ℏ) • (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j := by
rw [angularMomentumOperator_antisymm j i, neg_comp, smul_neg, ← neg_smul, ← neg_mul,
rw [angularMomentumCLM_antisymm j i, neg_comp, smul_neg, ← neg_smul, ← neg_mul,
← neg_mul, momentumSqr_comp_angularMomentum_commute]

private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add
Expand All @@ -194,7 +194,7 @@ private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add
= (-I * ℏ) • (𝐱 k ∘L 𝐩 l - δ[k,l] • (𝐱 ⬝ᵥ 𝐩)) ∘L (𝐩 ⬝ᵥ 𝐩) by
nth_rw 2 [← lie_skew]
simp_rw [this, ← sub_eq_add_neg, ← smul_sub, ← sub_comp, symm j i, sub_sub_sub_cancel_right,
momentumSqr_comp_angularMomentum_commute, angularMomentumOperator]
momentumSqr_comp_angularMomentum_commute, angularMomentumCLM]
intro k l
calc
_ = (𝐱 ⬝ᵥ 𝐩) ∘L ⁅𝐱 k, 𝐩 l⁆ ∘L (𝐩 ⬝ᵥ 𝐩) + 𝐱 k ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱[d] ⬝ᵥ 𝐩⁆ ∘L 𝐩 l
Expand Down Expand Up @@ -248,7 +248,7 @@ private lemma positionCompMomentumSqr_comm_radiusRegInvCompPosition_add
_ = 𝐫₀ ε (-1) ∘L (𝐱 i ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱 j⁆ - 𝐱 j ∘L ⁅𝐩[d] ⬝ᵥ 𝐩, 𝐱 i⁆) := by simp [hA]
_ = (-2 * I * ℏ) • 𝐫₀ ε (-1) ∘L 𝐋 i j := by
simp_rw [← lie_skew _ (𝐱 _), position_commutation_momentumSqr, comp_neg, comp_smul,
← neg_smul, ← neg_mul, ← smul_sub, comp_smul, angularMomentumOperator]
← neg_smul, ← neg_mul, ← smul_sub, comp_smul, angularMomentumCLM]

private lemma momentum_comm_radiusRegPow_position_symm {d : ℕ} (ε : ℝˣ) (s : ℝ) (i j : Fin d) :
⁅𝐩 i, 𝐫₀ ε s ∘L 𝐱 j⁆ = ⁅𝐩 j, 𝐫₀ ε s ∘L 𝐱 i⁆ := by
Expand All @@ -262,8 +262,8 @@ private lemma positionDotMomentumCompMomentum_comm_radiusRegInvCompPosition_add
nth_rw 2 [← lie_skew]
simp_rw [leibniz_lie, this,
momentum_comm_radiusRegPow_position_symm, ← sub_eq_add_neg, add_sub_add_left_eq_sub,
smul_comp, ← smul_sub, comp_assoc, ← comp_sub, angularMomentumOperator_antisymm i j, comp_neg,
smul_neg, neg_mul, neg_smul, angularMomentumOperator]
smul_comp, ← smul_sub, comp_assoc, ← comp_sub, angularMomentumCLM_antisymm i j, comp_neg,
smul_neg, neg_mul, neg_smul, angularMomentumCLM]
intro k
calc
_ = -(I * ℏ) • (ε.1 ^ 2) • 𝐫₀ ε (-1-2) ∘L 𝐱 k := by
Expand Down Expand Up @@ -330,7 +330,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) :
𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱 = (2 : ℝ) • (𝐱 ⬝ᵥ 𝐩) ∘L 𝐱 i + (-I * ℏ * (d - 3)) • 𝐱 i
+ ((-2 : ℝ) • 𝐫₀ ε 2 ∘L 𝐩 i + (2 * ε.1 ^ 2 : ℝ) • 𝐩 i) := by
-- Change summand
simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumOperator, comp_sub,
simp_rw [dotProduct, mul_def, ← Finset.sum_add_distrib, angularMomentumCLM, comp_sub,
sub_comp, comp_assoc, sub_add_sub_comm, momentum_comp_position_eq, comp_sub, comp_smul,
comp_id, ← comp_assoc, position_comp_commute i _, ← add_sub_assoc, ← two_smul ℝ,
sub_sub_eq_add_sub, sub_add_eq_add_sub, comp_assoc, comp_eq_comp_add_commute (𝐱 i) (𝐩 _),
Expand Down Expand Up @@ -425,14 +425,14 @@ private lemma sum_Lpp (d : ℕ) : ∑ i : Fin d, ∑ j, 𝐋 i j ∘L 𝐩 j ∘
rw [sum_symmetrize]
conv_lhs =>
enter [2, 2, i, 2, j]
rw [angularMomentumOperator_antisymm j i, momentum_comp_commute j i]
rw [angularMomentumCLM_antisymm j i, momentum_comp_commute j i]
simp

private lemma sum_ppL (d : ℕ) : ∑ i : Fin d, ∑ j, 𝐩 i ∘L 𝐩 j ∘L 𝐋 i j = 0 := by
rw [sum_symmetrize]
conv_lhs =>
enter [2, 2, i, 2, j]
rw [← comp_assoc, ← comp_assoc, angularMomentumOperator_antisymm j i, momentum_comp_commute j i]
rw [← comp_assoc, ← comp_assoc, angularMomentumCLM_antisymm j i, momentum_comp_commute j i]
simp

private lemma sum_LppL (d : ℕ) :
Expand All @@ -442,15 +442,15 @@ private lemma sum_LppL (d : ℕ) :
enter [2, 2, i, 2, j, 2, k]
calc
_ = (𝐋 i k ∘L 𝐩 k ∘L 𝐩 j - 𝐋 j k ∘L 𝐩 k ∘L 𝐩 i) ∘L 𝐋 i j := by
simp [angularMomentumOperator_antisymm j i, comp_neg, ← comp_assoc, sub_eq_add_neg]
simp [angularMomentumCLM_antisymm j i, comp_neg, ← comp_assoc, sub_eq_add_neg]
_ = (𝐱 i ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 j - 𝐱 k ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 j
- (𝐱 j ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 i - 𝐱 k ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 i)) ∘L 𝐋 i j := by
simp_rw [angularMomentumOperator, sub_comp, comp_assoc]
simp_rw [angularMomentumCLM, sub_comp, comp_assoc]
_ = (𝐱 i ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 k - 𝐱 j ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := by
simp_rw [momentum_comp_commute k, ← comp_assoc (𝐩 _), momentum_comp_commute k,
momentum_comp_commute i j, sub_sub_sub_cancel_right]
_ = 𝐋 i j ∘L (𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := by
simp_rw [← comp_assoc, ← sub_comp, angularMomentumOperator]
simp_rw [← comp_assoc, ← sub_comp, angularMomentumCLM]
trans (2 : ℂ)⁻¹ • ∑ i, ∑ j, 𝐋 i j ∘L (𝐩 ⬝ᵥ 𝐩) ∘L 𝐋 i j
· simp_rw [← comp_finsetSum, ← finsetSum_comp, ← comp_assoc, dotProduct, mul_def]
simp_rw [← comp_assoc, ← momentumSqr_comp_angularMomentum_commute, comp_assoc, ← comp_finsetSum,
Expand All @@ -464,9 +464,9 @@ private lemma sum_Lprx (d : ℕ) (ε : ℝˣ) :
enter [1, 2, 2, i, 2, j]
calc
_ = 𝐋 i j ∘L (𝐩 j ∘L 𝐱 i - 𝐩 i ∘L 𝐱 j) := by
simp [angularMomentumOperator_antisymm j i, comp_assoc, sub_eq_add_neg]
simp [angularMomentumCLM_antisymm j i, comp_assoc, sub_eq_add_neg]
_ = 𝐋 i j ∘L 𝐋 i j := by
simp [momentum_comp_position_eq, symm j i, angularMomentumOperator]
simp [momentum_comp_position_eq, symm j i, angularMomentumCLM]
rw [← angularMomentumSqr_comp_radiusRegPow_commute, angularMomentumOperatorSqr]

private lemma sum_rxpL (d : ℕ) (ε : ℝˣ) :
Expand All @@ -475,8 +475,8 @@ private lemma sum_rxpL (d : ℕ) (ε : ℝˣ) :
rw [sum_symmetrize]
conv_lhs =>
enter [2, 2, 2, i, 2, j]
rw [angularMomentumOperator_antisymm j i, comp_neg, comp_neg, ← sub_eq_add_neg, ← comp_assoc,
← comp_assoc, ← sub_comp, ← angularMomentumOperator]
rw [angularMomentumCLM_antisymm j i, comp_neg, comp_neg, ← sub_eq_add_neg, ← comp_assoc,
← comp_assoc, ← sub_comp, ← angularMomentumCLM]
rw [angularMomentumOperatorSqr]

private lemma sum_prx (d : ℕ) (ε : ℝˣ) :
Expand Down
12 changes: 8 additions & 4 deletions Physlib/QuantumMechanics/Operators/API-map.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,17 +127,21 @@ Requirements:

- description: "The components 𝐋ᵢⱼ = xᵢpⱼ - xⱼpᵢ of the angular momentum operator and the scalar 𝐋² are defined on Schwartz maps, with antisymmetry in the two indices and the vanishing of a repeated index, and the one-, two- and three-dimensional cases are treated separately."
done: true
location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumOperator, notation 𝐋, angularMomentumOperator_apply, angularMomentumOperator_antisymm, angularMomentumOperator_eq_zero, angularMomentumOperatorSqr, notation 𝐋², angularMomentumOperatorSqr_apply, angularMomentumOperator1D_trivial, angularMomentumOperator2D, angularMomentumOperator3D)"
location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumCLM, notation 𝐋, angularMomentumCLM_apply, angularMomentumCLM_antisymm, angularMomentumCLM_eq_zero, angularMomentumOperatorSqr, notation 𝐋², angularMomentumOperatorSqr_apply, angularMomentumOperator1D_trivial, angularMomentumOperator2D, angularMomentumOperator3D)"

- description: "Position and momentum transform as vectors under the angular momenta, which close into the Lie algebra of rotations."
done: true
location: "Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentum_commutation_position, angularMomentum_commutation_momentum, angularMomentum_commutation_angularMomentum)"
location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentum_commutation_position, angularMomentum_commutation_momentum, angularMomentum_commutation_angularMomentum)"

- description: "The scalar 𝐋² commutes with every angular momentum component, with the momentum squared and with any regularized power of the radius."
done: true
location: "Physlib/QuantumMechanics/Operators/Commutation.lean (angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_radiusRegPow)"
location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_momentumSqr, angularMomentumSqr_commutation_radiusRegPow, angularMomentum_commutation_momentumSqr, angularMomentum_commutation_radiusRegPow)"

- description: "The API shall carry angular momentum over from Schwartz maps, where it currently lives only as continuous linear maps, to the Hilbert space as a self-adjoint partially defined operator, with its spectrum, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions."
- description: "Each angular momentum component acts on the Hilbert space with dense Schwartz domain, agrees almost everywhere with its Schwartz-space action, preserves the Schwartz submodule, and is symmetric and closable."
done: true
location: "Physlib/QuantumMechanics/Operators/AngularMomentum.lean (angularMomentumOperator, angularMomentumOperator_domain_eq, angularMomentumOperator_apply, angularMomentumOperator_apply_ae, angularMomentumOperator_range, angularMomentumOperator_hasDenseDomain, angularMomentumCLM_eq_momentum_position, angularMomentumOperator_isSymmetric, angularMomentumOperator_isUnbounded)"

- description: "The API shall extend angular momentum from its Schwartz domain to self-adjoint operators on the Hilbert space, with their spectra, the raising and lowering operators, the eigenvalues ℏ² l (l + 1) of 𝐋² and ℏ m of a chosen component, and the spherical harmonics as the corresponding eigenfunctions."
done: false
location: N/A

Expand Down
Loading
Loading