Parity operator

The parity operator on functions

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

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.

The parity operator on Schwartz maps

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

The parity operator on the Schwartz maps is defined as the 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.

def QuantumMechanics.OneDimension.HilbertSpace.parityOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective

The unbounded parity operator, whose domain is Schwartz maps.

Equations

• QuantumMechanics.OneDimension.HilbertSpace.parityOperatorUnbounded = QuantumMechanics.OneDimension.UnboundedOperator.ofSelfCLM QuantumMechanics.OneDimension.HilbertSpace.parityOperatorSchwartz

@[simp]

theorem QuantumMechanics.OneDimension.HilbertSpace.parityOperatorSchwartz_parityOperatorSchwartz (ψ : SchwartzMap ℝ ℂ) : parityOperatorSchwartz (parityOperatorSchwartz ψ) = ψ

Parity operator is self adjoint

theorem QuantumMechanics.OneDimension.HilbertSpace.parityOperatorUnbounded_isSelfAdjoint : parityOperatorUnbounded.IsSelfAdjoint