feat: Laplace-Runge-Lenz vector#947
feat: Laplace-Runge-Lenz vector#947jstoobysmith merged 17 commits intolean-phys-community:masterfrom
Conversation
| @@ -23,4 +22,12 @@ def kronecker_delta [Ring R] (i j : Fin d) : R := if (i = j) then 1 else 0 | |||
| @[inherit_doc kronecker_delta] | |||
| macro "δ[" i:term "," j:term "]" : term => `(kronecker_delta $i $j) | |||
There was a problem hiding this comment.
can we rename kronecker_delta to kroneckerDelta.
| but is convenient to include for two reasons: | ||
| - It improves the convergence: `r(ε)⁻¹ + ½ε²r(ε)⁻³ = r⁻¹(1 + O(ε⁴/r⁴))` with no `O(ε²/r²)` term. | ||
| - It is what appears in the commutators of the (regularized) LRL vector components. | ||
|
|
There was a problem hiding this comment.
Is there a reference for the regularized hamiltonian we could put here?
There was a problem hiding this comment.
I have not been able to find one, but will continue searching.
|
|
||
| -/ | ||
|
|
||
| private def xp := ∑ i : Fin H.d, 𝐱[i] ∘L 𝐩[i] |
There was a problem hiding this comment.
could we give these more descriptive names, e.g. positionDotMomentum, and doc-strings? Same with f1, f2 etc below.
|
|
||
| -/ | ||
|
|
||
| private lemma lrlOperator_eq' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐋[i,j] ∘L 𝐩[j] |
There was a problem hiding this comment.
could these be moved up to closer to the definition of the lrlOperator, also I don't see a reason why these should be private.
| dsimp only [Bracket.bracket] | ||
| simp only [ContinuousLinearMap.mul_def, comp_assoc, comp_sub, sub_comp, sub_add_sub_cancel'] | ||
|
|
||
| lemma commute (A B : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) : A ∘L B = B ∘L A + ⁅A, B⁆ := by |
There was a problem hiding this comment.
maybe comp_eq_comp_add_commute
| dsimp only [Bracket.bracket] | ||
| simp only [ContinuousLinearMap.mul_def, add_sub_cancel] | ||
|
|
||
| lemma commute' (A B : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ)) : A ∘L B = B ∘L A - ⁅B, A⁆ := by |
| ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply, positionOperator_apply] | ||
| ring | ||
|
|
||
| lemma position_position_eq {d : ℕ} (i j : Fin d) : 𝐱[i] ∘L 𝐱[j] = 𝐱[j] ∘L 𝐱[i] := by |
There was a problem hiding this comment.
position_comp_commute? (Less sure about this one)
| lemma positionOperator_apply {d : ℕ} (i : Fin d) (ψ : 𝓢(Space d, ℂ)) (x : Space d) : | ||
| 𝐱[i] ψ x = x i * ψ x := rfl | ||
| /-- Power of regularized norm, `(‖x‖² + ε²)^(s/2)` -/ | ||
| private def normRegularizedPow (ε s : ℝ) : Space d → ℝ := |
There was a problem hiding this comment.
We have a file in SpaceTime in ./Space/Norm.lean that does something similar to this, although uses a different regularization. I think the regularization you have here is probably better, and maybe it is worth combining some of the results here and there.
There was a problem hiding this comment.
I've left a TODO to revisit this. I see some pros and cons to both, e.g. 0 < ε is needed repeatedly and continuous ε vs discrete n.
|
Thanks for the feedback; I've made improvements to the def/lemma names and organization. |
|
This looks good to me! Though I want to take another quick Look tomorrow before approving it - sorry, I ran out of time today. |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Approved - many thanks. Will merge shortly
jstoobysmith
added
the
ready-to-merge
2 participants
Refactors
positionOperatorusing newSchwartzMap.smulLeftCLMand adds...r(ε)ˢwhich mapψto(‖x‖² + ε²) ^ (s/2) ψ.r(ε)⁻¹.A² = 2mH(L² + (ℏ(d-1)/2)²) + m²k² + ε²(...).The LRL file is long but mostly consists of private lemmas to split up the straightforward yet tedious calculations for the commutators and square of LRL vector.