PhysLean Documentation

PhysLean.QuantumMechanics.OneDimension.Operators.Position

Position operator #

In this module we define:

We show that position wavefunctions are generalized eigenvectors of the position operator.

The position operator on functions ℝ → ℂ #

source
def QuantumMechanics.OneDimension.positionOperator :
(ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ

The position operator is defined as the linear map from ℝ → ℂ to ℝ → ℂ taking ψ to x * ψ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The position operator on Schwartz maps #

    source
    def QuantumMechanics.OneDimension.positionOperatorSchwartz :
    SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

    The parity operator on the Schwartz maps is defined as the linear map from 𝓢(ℝ, ℂ) to itself, such that ψ is taken to fun x => x * ψ x.

    Equations
    Instances For
      source
      theorem QuantumMechanics.OneDimension.positionOperatorSchwartz_apply_fun (ψ : SchwartzMap ℝ ℂ) :
      ⇑(positionOperatorSchwartz ψ) = fun (x : ℝ) => ↑x * ψ x
      source
      @[simp]
      theorem QuantumMechanics.OneDimension.positionOperatorSchwartz_apply (ψ : SchwartzMap ℝ ℂ) (x : ℝ) :
      (positionOperatorSchwartz ψ) x = ↑x * ψ x
      source
      def QuantumMechanics.OneDimension.positionOperatorUnbounded :
      UnboundedOperator HilbertSpace.schwartzIncl HilbertSpace.schwartzIncl_injective

      The unbounded position operator, whose domain is Schwartz maps.

      Equations
      Instances For

        Generalized eigenvectors of the momentum operator #

        source
        theorem QuantumMechanics.OneDimension.positionStates_generalized_eigenvector_positionOperatorUnbounded (x : ℝ) :
        positionOperatorUnbounded.IsGeneralizedEigenvector (HilbertSpace.positionState x) ↑x

        Position operator is self adjoint #

        source
        theorem QuantumMechanics.OneDimension.positionOperatorUnbounded_isSelfAdjoint :
        positionOperatorUnbounded.IsSelfAdjoint