PhysLean Documentation

PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum

Angular momentum operator #

i. Overview #

In this module we introduce several angular momentum operators for quantum mechanics on Space d.

ii. Key results #

Definitions:

Notation:

iii. Table of contents #

iv. References #

A. Angular momentum operator #

source
def QuantumMechanics.angularMomentumOperator {d : β„•} (i j : Fin d) :
SchwartzMap (Space d) β„‚ β†’L[β„‚] SchwartzMap (Space d) β„‚

Component i j of the angular momentum operator is the continuous linear map from 𝓒(Space d, β„‚) to itself defined by 𝐋ᡒⱼ ≔ 𝐱ᡒ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᡒ.

Equations
Instances For
    source
    def QuantumMechanics.Β«term𝐋[_,_]Β» :
    Lean.ParserDescr

    Component i j of the angular momentum operator is the continuous linear map from 𝓒(Space d, β„‚) to itself defined by 𝐋ᡒⱼ ≔ 𝐱ᡒ∘𝐩ⱼ - 𝐱ⱼ∘𝐩ᡒ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem QuantumMechanics.angularMomentumOperator_apply_fun {d : β„•} (i j : Fin d) (ψ : SchwartzMap (Space d) β„‚) :
      𝐋[i,j] ψ = 𝐱[i] (𝐩[j] ψ) - 𝐱[j] (𝐩[i] ψ)
      source
      theorem QuantumMechanics.angularMomentumOperator_apply {d : β„•} (i j : Fin d) (ψ : SchwartzMap (Space d) β„‚) (x : Space d) :
      (𝐋[i,j] ψ) x = (𝐱[i] (𝐩[j] ψ)) x - (𝐱[j] (𝐩[i] ψ)) x

      A.1 Antisymmetry #

      source
      theorem QuantumMechanics.angularMomentumOperator_antisymm {d : β„•} (i j : Fin d) :
      𝐋[i,j] = -𝐋[j,i]

      The angular momentum operator is antisymmetric, 𝐋ᡒⱼ = -𝐋ⱼᡒ

      source
      theorem QuantumMechanics.angularMomentumOperator_eq_zero {d : β„•} (i : Fin d) :
      𝐋[i,i] = 0

      Angular momentum operator components with repeated index vanish, 𝐋ᡒᡒ = 0.

      B. Angular momentum squared operator #

      source
      def QuantumMechanics.angularMomentumOperatorSqr {d : β„•} :
      SchwartzMap (Space d) β„‚ β†’L[β„‚] SchwartzMap (Space d) β„‚

      The square of the angular momentum operator, 𝐋² ≔ Β½ βˆ‘α΅’β±Ό π‹α΅’β±Όβˆ˜π‹α΅’β±Ό.

      Equations
      Instances For
        source
        def QuantumMechanics.Β«term𝐋²» :
        Lean.ParserDescr

        The square of the angular momentum operator, 𝐋² ≔ Β½ βˆ‘α΅’β±Ό π‹α΅’β±Όβˆ˜π‹α΅’β±Ό.

        Equations
        Instances For
          source
          theorem QuantumMechanics.angularMomentumOperatorSqr_apply_fun {d : β„•} (ψ : SchwartzMap (Space d) β„‚) :
          𝐋² ψ = 2⁻¹ β€’ βˆ‘ i : Fin d, βˆ‘ j : Fin d, 𝐋[i,j] (𝐋[i,j] ψ)
          source
          theorem QuantumMechanics.angularMomentumOperatorSqr_apply {d : β„•} (ψ : SchwartzMap (Space d) β„‚) (x : Space d) :
          (𝐋² ψ) x = 2⁻¹ * βˆ‘ i : Fin d, βˆ‘ j : Fin d, (𝐋[i,j] (𝐋[i,j] ψ)) x

          C. Special cases in low dimensions #

          β€’ d = 1 : The angular momentum operator is trivial.

          β€’ d = 2 : The angular momentum operator has only one independent component, 𝐋₀₁, which may be thought of as a (pseudo)scalar operator.

          β€’ d = 3 : The angular momentum operator has three independent components, 𝐋₀₁, 𝐋₁₂ and 𝐋₂₀. Dualizing using the Levi-Civita symbol produces the familiar (pseudo)vector angular momentum operator with components 𝐋₀ = 𝐋₁₂, 𝐋₁ = 𝐋₂₀ and 𝐋₂ = 𝐋₀₁.

          source
          theorem QuantumMechanics.angularMomentumOperator1D_trivial (i j : Fin 1) :
          𝐋[i,j] = 0

          In one dimension the angular momentum operator is trivial.

          source
          def QuantumMechanics.angularMomentumOperator2D :
          SchwartzMap (Space 2) β„‚ β†’L[β„‚] SchwartzMap (Space 2) β„‚

          The angular momentum (pseudo)scalar operator in two dimensions, 𝐋 ≔ 𝐋₀₁.

          Equations
          Instances For
            source
            def QuantumMechanics.angularMomentumOperator3D (i : Fin 3) :
            SchwartzMap Space β„‚ β†’L[β„‚] SchwartzMap Space β„‚

            The angular momentum (pseudo)vector operator in three dimension, 𝐋ᡒ ≔ Β½ βˆ‘β±Όβ‚– Ξ΅α΅’β±Όβ‚– 𝐋ⱼₖ.

            Equations
            Instances For