Schwartz submodule of the Hilbert space

This can be used to define e.g. the rigged Hilbert space.

def QuantumMechanics.OneDimension.HilbertSpace.schwartzIncl : SchwartzMap ℝ ℂ →L[ℂ] ↥HilbertSpace

The continuous linear map including Schwartz functions into the hilbert space.

Equations

• QuantumMechanics.OneDimension.HilbertSpace.schwartzIncl = SchwartzMap.toLpCLM ℂ ℂ 2 MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HilbertSpace.schwartzIncl_injective : Function.Injective ⇑schwartzIncl

theorem QuantumMechanics.OneDimension.HilbertSpace.schwartzIncl_coe_ae (ψ : SchwartzMap ℝ ℂ) : ψ.toFun =ᵐ[MeasureTheory.volume] ↑↑(schwartzIncl ψ)

theorem QuantumMechanics.OneDimension.HilbertSpace.schwartzIncl_inner (ψ1 ψ2 : SchwartzMap ℝ ℂ) : inner ℂ (schwartzIncl ψ1) (schwartzIncl ψ2) = ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * ψ2 x