Position states

We define plane waves as a member of the dual of the Schwartz submodule of the Hilbert space.

def QuantumMechanics.OneDimension.HilbertSpace.positionState (x : ℝ) : SchwartzMap ℝ ℂ →L[ℂ] ℂ

Position state as a member of the dual of the Schwartz submodule of the Hilbert space.

Equations

• QuantumMechanics.OneDimension.HilbertSpace.positionState x = SchwartzMap.delta ℂ ℂ x

theorem QuantumMechanics.OneDimension.HilbertSpace.positionState_apply (x : ℝ) (ψ : SchwartzMap ℝ ℂ) : (positionState x) ψ = ψ x

theorem QuantumMechanics.OneDimension.HilbertSpace.eq_of_eq_positionState {ψ1 ψ2 : SchwartzMap ℝ ℂ} (h : ∀ (x : ℝ), (positionState x) ψ1 = (positionState x) ψ2) : ψ1 = ψ2

Two elements of the 𝓢(ℝ, ℂ) are equal if they are equal on all position states.