Parity operator

def QuantumMechanics.OneDimension.HilbertSpace.parity : (ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ

The parity operator is defined as linear map from ℝ → ℂ to itself, such that ψ is taken to fun x => ψ (-x).

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumMechanics.OneDimension.HilbertSpace.memHS_of_parity (ψ : ℝ → ℂ) (hψ : MemHS ψ) : MemHS (parity ψ)

The parity operator acting on a member of the Hilbert space is in Hilbert space.