1. Physlib
  2. QuantumMechanics
  3. HilbertSpaces
  4. OneDimension
  5. PositionStates
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

Position states

We define position state as a member of the dual of the Schwartz submodule of the 1d Hilbert space.

This module has been generalized to d-dimensions in QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean and will be removed in the near future.

@[expose] public section

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

def positionState (x : ℝ) : 𝓢(ℝ, ℂ) →L[ℂ] ℂ := TemperedDistribution.delta x
lemma positionState_apply (x : ℝ) (ψ : 𝓢(ℝ, ℂ)) : positionState x ψ = ψ x := rfl

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

lemma eq_of_eq_positionState {ψ1 ψ2 : 𝓢(ℝ, ℂ)} (h : ∀ x, positionState x ψ1 = positionState x ψ2) : ψ1 = ψ2 := ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)h:∀ (x : ℝ), (positionState x) ψ1 = (positionState x) ψ2⊢ ψ1 = ψ2 ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)h:∀ (x : ℝ), (positionState x) ψ1 = (positionState x) ψ2x:ℝ⊢ ψ1 x = ψ2 x All goals completed! 🐙