Skip to content

feat(LaplaceRungeLenzVector): prove angularMomentum_commutation_lrl #991

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

Open
pitmonticone wants to merge 4 commits into
base: master
Choose a base branch
from
+34 −4
Open

feat(LaplaceRungeLenzVector): prove angularMomentum_commutation_lrl #991

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
aef181c
feat(LaplaceRungeLenzVector): prove `angularMomentum_commutation_lrl`
pitmonticone Mar 14, 2026
9eff056
refactor(LaplaceRungeLenzVector): address review comments
pitmonticone Mar 15, 2026
971f6d3
fix(LaplaceRungeLenzVector): restore split simp calls (combining brea…
pitmonticone Mar 15, 2026
88d554e
refactor(LaplaceRungeLenzVector): remove unused simp args, drop unuse…
pitmonticone Mar 17, 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
38 changes: 34 additions & 4 deletions PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,14 +136,45 @@ private def constRadiusRegInvCompPosition (ε : ℝˣ) (i : Fin H.d) :=
-/

/-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/
@[sorryful]
lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) :
⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j
- (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by
sorry
simp only [lrlOperator_eq' H ε]
simp only [lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz]
simp only [angularMomentum_commutation_angularMomentum,
angularMomentum_commutation_momentum,
angularMomentum_commutation_radiusRegPow,
angularMomentum_commutation_position]
dsimp only [kroneckerDelta]
simp only [comp_sub, comp_smul, zero_comp, add_zero,
smul_sub, smul_add, smul_smul]
simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero,
ite_smul, zero_smul, smul_ite, smul_zero,
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j]
simp only [neg_comp, smul_neg]
have ite_comp_right : ∀ (p : Prop) [Decidable p]
(A B : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)),
(if p then A else 0).comp B = if p then A.comp B else 0 :=
fun p _ A B ↦ by split_ifs <;> simp
simp only [ite_comp_right,
sub_comp, add_comp, smul_comp,
Finset.sum_add_distrib, Finset.sum_sub_distrib,
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
rw [angularMomentumOperator_antisymm i k, angularMomentumOperator_antisymm j k]
simp only [neg_comp, smul_neg, neg_neg]
split_ifs with hik hjk <;>
simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, zero_mul,
Finset.sum_const_zero, add_zero, sub_self, neg_zero, neg_neg,
← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] <;>
(try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)]) <;>
(try conv_lhs => rw [show
2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1) * (Complex.I * ↑↑ℏ) =
Complex.I * ↑↑ℏ * (2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1)) from by ring]) <;>
abel
Comment on lines 138 to +175
Copy link
Copy Markdown
Contributor

@adomasbaliuka adomasbaliuka Apr 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

how about this (I couldn't further combine the simps without breaking it)

Suggested change
/-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/
@[sorryful]
lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) :
⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j
- (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by
sorry
simp only [lrlOperator_eq' H ε]
simp only [lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz]
simp only [angularMomentum_commutation_angularMomentum,
angularMomentum_commutation_momentum,
angularMomentum_commutation_radiusRegPow,
angularMomentum_commutation_position]
dsimp only [kroneckerDelta]
simp only [comp_sub, comp_smul, zero_comp, add_zero,
smul_sub, smul_add, smul_smul]
simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero,
ite_smul, zero_smul, smul_ite, smul_zero,
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j]
simp only [neg_comp, smul_neg]
have ite_comp_right : ∀ (p : Prop) [Decidable p]
(A B : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)),
(if p then A else 0).comp B = if p then A.comp B else 0 :=
fun p _ A B ↦ by split_ifs <;> simp
simp only [ite_comp_right,
sub_comp, add_comp, smul_comp,
Finset.sum_add_distrib, Finset.sum_sub_distrib,
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
rw [angularMomentumOperator_antisymm i k, angularMomentumOperator_antisymm j k]
simp only [neg_comp, smul_neg, neg_neg]
split_ifs with hik hjk <;>
simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, zero_mul,
Finset.sum_const_zero, add_zero, sub_self, neg_zero, neg_neg,
← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] <;>
(try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)]) <;>
(try conv_lhs => rw [show
2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1) * (Complex.I * ↑↑ℏ) =
Complex.I * ↑↑ℏ * (2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1)) from by ring]) <;>
abel
/-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/
lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) :
⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j
- (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by
simp only [lrlOperator_eq, lie_sub, lie_add, lie_leibniz, angularMomentum_commutation_momentumSqr,
angularMomentum_commutation_position, angularMomentum_commutation_momentum, lie_sum, lie_smul,
angularMomentum_commutation_radiusRegPow]
simp only [comp_zero, smul_sub, sub_comp, smul_comp, zero_add, comp_sub, comp_smul,
Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum, sum_smul, zero_comp,
add_zero]
simp only [sub_add_sub_cancel, sub_self, zero_comp, add_zero, ← Nat.cast_smul_eq_nsmul ℂ, smul_smul]
ext f x
simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply,
ContinuousLinearMap.smul_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, smul_eq_mul, real_smul, ofReal_mul]
ring

Copy link
Copy Markdown
Member

@jstoobysmith jstoobysmith Apr 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me! Will give @pitmonticone chance to comment here. This PR currently has a merge conflict (since ./PhysLean got renamed to ./PhysLib), which will also need addressing (maybe easier to open a new PR).


/-- `⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0` -/
@[sorryful]
lemma angularMomentum_commutation_lrlSqr (ε : ℝˣ) (i j : Fin H.d) :
⁅𝐋[i,j], H.lrlOperatorSqr ε⁆ = 0 := by
unfold lrlOperatorSqr
Expand All @@ -153,7 +184,6 @@ lemma angularMomentum_commutation_lrlSqr (ε : ℝˣ) (i j : Fin H.d) :
simp [Finset.sum_add_distrib, Finset.sum_sub_distrib]

/-- `⁅𝐋², 𝐀(ε)²⁆ = 0` -/
@[sorryful]
lemma angularMomentumSqr_commutation_lrlSqr (ε : ℝˣ) :
⁅angularMomentumOperatorSqr (d := H.d), H.lrlOperatorSqr ε⁆ = 0 := by
unfold angularMomentumOperatorSqr
Expand Down
Loading