Research proof index

The unbounded momentum operator, whose domain is Schwartz maps. -/ def momentumOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective := UnboundedOperator.ofSelfCLM momentumOperatorSchwartz /-! ## Generalized eigenvectors of the momentum operator -/ lemma planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded (k : ℝ) : mo...

The unbounded momentum operator, whose domain is Schwartz maps. -/ def momentumOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective := UnboundedOperator.ofSelfCLM momentumOperatorSchwartz /-! ## Generalized eigenvectors of the momentum operator

The canonical commutation relations: [xᵢ, pⱼ] = iℏ δᵢⱼ𝟙.

x ↦ ‖x‖ˢψ(x) is square-integrable provided s is not too negative.

𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 except perhaps at x = 0.

𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 provided 𝐫[ε,s] ψ 0 is bounded.