Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersQuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl
Plain-language statement
⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏk·ε²𝐫(ε)⁻³𝐩ᵢ - 3ℏ²k/2·ε²𝐫(ε)⁻⁵𝐱ᵢ
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.HydrogenAtom.lrl_commutation_lrl
Plain-language statement
⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = (-2iℏm·𝐇(ε) + iℏmkε²·𝐫(ε)⁻³)𝐋ᵢⱼ
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.HydrogenAtom.lrlOperator_eq
Plain-language statement
𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.HydrogenAtom.lrlOperator_eq''
Plain-language statement
𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq
Plain-language statement
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ℏ²ε²𝐫(ε)⁻³.
Source project: Physlib
Person-level attribution pending.