Momentum operator #
In this module we define:
- The momentum operator on functions
ℝ → ℂ
- The momentum operator on Schwartz maps as an unbounded operator on the Hilbert space.
We show that plane waves are generalized eigenvectors of the momentum operator.
The momentum operator on functions ℝ → ℂ
#
The momentum operator is defined as the map from ℝ → ℂ
to ℝ → ℂ
taking
ψ
to - i ℏ ψ'
.
Equations
Instances For
theorem
QuantumMechanics.OneDimension.continuous_momentumOperator
(ψ : ℝ → ℂ)
(hψ : ContDiff ℝ 1 ψ)
:
theorem
QuantumMechanics.OneDimension.momentumOperator_smul
{ψ : ℝ → ℂ}
(hψ : Differentiable ℝ ψ)
(c : ℂ)
:
theorem
QuantumMechanics.OneDimension.momentumOperator_add
{ψ1 ψ2 : ℝ → ℂ}
(hψ1 : Differentiable ℝ ψ1)
(hψ2 : Differentiable ℝ ψ2)
:
The momentum operator on Schwartz maps #
The parity operator on the Schwartz maps is defined as the linear map from
𝓢(ℝ, ℂ)
to itself, such that ψ
is taken to fun x => - I ℏ * ψ' x
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumMechanics.OneDimension.momentumOperatorSchwartz_apply
(ψ : SchwartzMap ℝ ℂ)
(x : ℝ)
:
The unbounded momentum operator, whose domain is Schwartz maps.