Plane waves

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

def QuantumMechanics.OneDimension.HilbertSpace.planewaveFunctional (k : ℝ) : SchwartzMap ℝ ℂ →L[ℂ] ℂ

Plane waves as a member of the dual of the Schwartz submoudle of the Hilbert space.

For a given k this corresponds to the plane wave exp (2π I k x).

Equations

• QuantumMechanics.OneDimension.HilbertSpace.planewaveFunctional k = (SchwartzMap.delta ℂ ℂ k).comp (SchwartzMap.fourierTransformCLM ℂ)

theorem QuantumMechanics.OneDimension.HilbertSpace.planewaveFunctional_apply (k : ℝ) (ψ : SchwartzMap ℝ ℂ) : (planewaveFunctional k) ψ = Real.fourierIntegral (⇑ψ) k

theorem QuantumMechanics.OneDimension.HilbertSpace.eq_of_eq_planewaveFunctional {ψ1 ψ2 : SchwartzMap ℝ ℂ} (h : ∀ (k : ℝ), (planewaveFunctional k) ψ1 = (planewaveFunctional k) ψ2) : ψ1 = ψ2

Two elements of the Schwartz submodule are equal if and only if they are equal on all applications of planewaveFunctional.