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 ε).comp 𝐋[i,j]

⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = -iℏ 2m 𝐇(ε)𝐋ᵢⱼ

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

⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/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 * H.k) ^ 2 • ContinuousLinearMap.id ℂ (SchwartzMap (Space H.d) ℂ) - ((H.m * H.k) ^ 2 * ↑ε ^ 2) • 𝐫[ε,-2] + (H.m * H.k * ↑ε ^ 2) • 𝐫[ε,-3].comp (𝐋² + (4⁻¹ * ↑Constants.ℏ ^ 2 * (↑H.d - 1) * (↑H.d - 3)) • ContinuousLinearMap.id ℂ (SchwartzMap (Space H.d) ℂ))

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² - m²k²ε²𝐫(ε)⁻² + mkε²𝐫(ε)⁻³(𝐋² + ¼ℏ²(d-1)(d-3)).