Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Basic
public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
public import Physlib.Meta.TODO.BasicSchwartz submodule of the Hilbert space
This can be used to define e.g. the rigged Hilbert space.
TODO "Remove 1d Schwartz submodule once dependencies are all generalized to SpaceDHilbertSpace."@[expose] public sectionThe continuous linear map including Schwartz functions into the hilbert space.
def schwartzIncl : 𝓢(ℝ, ℂ) →L[ℂ] HilbertSpace :=
SchwartzMap.toLpCLM ℂ (E := ℝ) ℂ 2 MeasureTheory.volumelemma schwartzIncl_injective : Function.Injective schwartzIncl :=
SchwartzMap.injective_toLp _ _lemma schwartzIncl_coe_ae (ψ : 𝓢(ℝ, ℂ)) :
ψ.1 =ᶠ[ae volume] (schwartzIncl ψ) := (SchwartzMap.coeFn_toLp _ 2 volume).symmψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)h1✝:ψ1.toFun =ᵐ[volume] ↑↑(schwartzIncl ψ1)h2✝:ψ2.toFun =ᵐ[volume] ↑↑(schwartzIncl ψ2)a✝:ℝh1:ψ1.toFun a✝ = ↑↑(schwartzIncl ψ1) a✝h2:ψ2.toFun a✝ = ↑↑(schwartzIncl ψ2) a✝⊢ (starRingEnd ℂ) (ψ1.toFun a✝) * ψ2.toFun a✝ = (starRingEnd ℂ) (ψ1 a✝) * ψ2 a✝
All goals completed! 🐙