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 Mathlib.Analysis.Distribution.TemperedDistribution
public import Physlib.Meta.TODO.BasicPlane waves
We define plane waves as a member of the dual of the Schwartz submodule of the Hilbert space.
TODO "Generalize plane waves to d dimensions and SpaceDHilbertSpace."@[expose] public sectionPlane waves as a member of the dual of the Schwartz submodule of the Hilbert space.
For a given k this corresponds to the plane wave
exp (2π I k x).
def planewaveFunctional (k : ℝ) : 𝓢(ℝ, ℂ) →L[ℂ] ℂ :=
(TemperedDistribution.delta k : SchwartzMap ℝ ℂ →L[ℂ] ℂ) ∘L (SchwartzMap.fourierTransformCLM ℂ)
Two elements of the Schwartz submodule are equal if and only if they are equal on
all applications of planewaveFunctional.
lemma eq_of_eq_planewaveFunctional {ψ1 ψ2 : 𝓢(ℝ, ℂ)}
(h : ∀ k, planewaveFunctional k ψ1 = planewaveFunctional k ψ2) :
ψ1 = ψ2 :=
(FourierTransform.fourierCLE ℂ 𝓢(ℝ, ℂ)).injective (SchwartzMap.ext h)