Laplace-Runge-Lenz vector

In this file we define

• The (regularized) LRL vector operator for the quantum mechanical hydrogen atom, 𝐀(ε)ᵢ ≔ ½(𝐩ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐩ⱼ) - mk·𝐫(ε)⁻¹𝐱ᵢ.
• The square of the LRL vector operator, 𝐀(ε)² ≔ 𝐀(ε)ᵢ𝐀(ε)ᵢ.

The main results are

• The commutators ⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ) in angularMomentum_commutation_lrl
• The commutators ⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = -iℏ 2m 𝐇(ε)𝐋ᵢⱼ in lrl_commutation_lrl
• The commutators ⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏε²(⋯) in hamiltonianReg_commutation_lrl
• The relation 𝐀(ε)² = 2m 𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k² + ε²(⋯) in lrlOperatorSqr_eq

def QuantumMechanics.HydrogenAtom.lrlOperator (H : HydrogenAtom) (ε : ℝˣ) (i : Fin H.d) : SchwartzMap (Space H.d) ℂ →L[ℂ] SchwartzMap (Space H.d) ℂ

The (regularized) Laplace-Runge-Lenz vector operator for the d-dimensional hydrogen atom, 𝐀(ε)ᵢ ≔ ½(𝐩ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐩ⱼ) - mk·𝐫(ε)⁻¹𝐱ᵢ.

Equations

• H.lrlOperator ε i = 2⁻¹ • ∑ j : Fin H.d, (𝐩[j].comp 𝐋[i,j] + 𝐋[i,j].comp 𝐩[j]) - (H.m * H.k) • 𝐫[ε,-1].comp 𝐱[i]

def QuantumMechanics.HydrogenAtom.lrlOperatorSqr (H : HydrogenAtom) (ε : ℝˣ) : SchwartzMap (Space H.d) ℂ →L[ℂ] SchwartzMap (Space H.d) ℂ

The square of the LRL vector operator, 𝐀(ε)² ≔ 𝐀(ε)ᵢ𝐀(ε)ᵢ.

Equations

• H.lrlOperatorSqr ε = ∑ i : Fin H.d, (H.lrlOperator ε i).comp (H.lrlOperator ε i)

theorem QuantumMechanics.HydrogenAtom.lrlOperator_eq (H : HydrogenAtom) (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = 𝐱[i].comp 𝐩² - (∑ j : Fin H.d, 𝐱[j].comp 𝐩[j]).comp 𝐩[i] + (2⁻¹ * Complex.I * ↑↑Constants.ℏ * (↑H.d - 1)) • 𝐩[i] - (H.m * H.k) • 𝐫[ε,-1].comp 𝐱[i]

𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

theorem QuantumMechanics.HydrogenAtom.lrlOperator_eq' (H : HydrogenAtom) (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = ∑ j : Fin H.d, 𝐋[i,j].comp 𝐩[j] + (2⁻¹ * Complex.I * ↑↑Constants.ℏ * (↑H.d - 1)) • 𝐩[i] - (H.m * H.k) • 𝐫[ε,-1].comp 𝐱[i]

𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

theorem QuantumMechanics.HydrogenAtom.lrlOperator_eq'' (H : HydrogenAtom) (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = ∑ j : Fin H.d, 𝐩[j].comp 𝐋[i,j] - (2⁻¹ * Complex.I * ↑↑Constants.ℏ * (↑H.d - 1)) • 𝐩[i] - (H.m * H.k) • 𝐫[ε,-1].comp 𝐱[i]

𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

theorem QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl (H : HydrogenAtom) (ε : ℝˣ) (i j k : Fin H.d) : ⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ↑↑Constants.ℏ * ↑δ[i,k]) • H.lrlOperator ε j - (Complex.I * ↑↑Constants.ℏ * ↑δ[j,k]) • H.lrlOperator ε i

⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)

theorem QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrlSqr (H : HydrogenAtom) (ε : ℝˣ) (i j : Fin H.d) : ⁅𝐋[i,j], H.lrlOperatorSqr ε⁆ = 0

⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0

theorem QuantumMechanics.HydrogenAtom.angularMomentumSqr_commutation_lrlSqr (H : HydrogenAtom) (ε : ℝˣ) : ⁅𝐋², H.lrlOperatorSqr ε⁆ = 0

⁅𝐋², 𝐀(ε)²⁆ = 0

theorem QuantumMechanics.HydrogenAtom.lrl_commutation_lrl (H : HydrogenAtom) (ε : ℝˣ) (i j : Fin H.d) : ⁅H.lrlOperator ε i, H.lrlOperator ε j⁆ = ((-2 * Complex.I * ↑↑Constants.ℏ * ↑H.m) • H.hamiltonianReg ε + (Complex.I * ↑↑Constants.ℏ * ↑H.m * ↑H.k * ↑↑ε ^ 2) • 𝐫[ε,-3]).comp 𝐋[i,j]

⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = (-2iℏm·𝐇(ε) + iℏmkε²·𝐫(ε)⁻³)𝐋ᵢⱼ

theorem QuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl (H : HydrogenAtom) (ε : ℝˣ) (i : Fin H.d) : ⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ↑↑Constants.ℏ * ↑H.k * ↑↑ε ^ 2) • 𝐫[ε,-3].comp 𝐩[i] - (3 / 2 * ↑Constants.ℏ ^ 2 * H.k * ↑ε ^ 2) • 𝐫[ε,-5].comp 𝐱[i]

⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏk·ε²𝐫(ε)⁻³𝐩ᵢ - 3ℏ²k/2·ε²𝐫(ε)⁻⁵𝐱ᵢ

theorem QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq (H : HydrogenAtom) (ε : ℝˣ) : H.lrlOperatorSqr ε = (2 * H.m) • (H.hamiltonianReg ε).comp (𝐋² + (4⁻¹ * ↑Constants.ℏ ^ 2 * (↑H.d - 1) ^ 2) • ContinuousLinearMap.id ℂ (SchwartzMap (Space H.d) ℂ)) + (H.m ^ 2 * H.k ^ 2) • (ContinuousLinearMap.id ℂ (SchwartzMap (Space H.d) ℂ) - ↑ε ^ 2 • 𝐫[ε,-2]) - (2⁻¹ * ↑Constants.ℏ ^ 2 * H.m * H.k * (↑H.d - 1) * ↑ε ^ 2) • 𝐫[ε,-3]

The square of the (regularized) LRL vector operator is related to the (regularized) Hamiltonian 𝐇(ε) of the hydrogen atom, square of the angular momentum 𝐋² and powers of 𝐫(ε) as 𝐀(ε)² = 2m·𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k²(𝟙 - ε²·𝐫(ε)⁻²) - ½(d-1)mkℏ²ε²𝐫(ε)⁻³.