API: QM system on Space

Key data structure

The key data structure here corresponds to Hilbert space of 'square integrable functions from Space d to the complex numbers`. Really one will need the equivalence class of such functions.

• is defined

Need

This API will be used in, for example, the study of the classical harmonic oscillator, the reflectionless potential and other problems based on potentials in space.

Requirements

• The API shall contain the definition of the position operator
• The API shall contain the definition of the momentum operator
• The key data structure shall carry the instance of a Hilbert space
• The API shall contain the definition of a bra

Corresponding file system

Aspects of this API already exist, however, they are not structured neatly around the key data structure.

https://github.com/HEPLean/PhysLean/tree/master/PhysLean/QuantumMechanics/OneDimension

Parent APIs

#854

Read the existing API under PhysLean/QuantumMechanics/OneDimension and the parent API in issue #854 first. Define the key Hilbert-space data structure and determine how the position, momentum, bra, and Hilbert-space instance requirements should fit around it; done means all listed requirements are represented in the API.