diff --git a/Physlib/QuantumMechanics/HilbertSpaces/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/API-map.yaml new file mode 100644 index 000000000..e47c1670a --- /dev/null +++ b/Physlib/QuantumMechanics/HilbertSpaces/API-map.yaml @@ -0,0 +1,58 @@ +version: v0.1 + +Title: Hilbert spaces + +Overview: | + The central mathematical structure of non-relativistic quantum mechanics is the Hilbert space + (i.e. complete inner product space): quantum states are vectors in Hilbert spaces and + observables are self-adjoint operators acting on Hilbert spaces. Hilbert spaces for composite + systems can be constructed by taking tensor products/powers and completions of simpler spaces. + +ParentAPIs: + +References: + +Requirements: + + - description: + Defines the complete tensor product of a pair of Hilbert spaces. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/CompleteTensorProduct.lean (CompleteTensorProduct) + + - description: + Provides a linear isometry equivalence expressing the commutativity of the complete tensor + product of a pair of Hilbert spaces. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/CompleteTensorProduct.lean (CompleteTensorProduct.comm) + + - description: + Provides a linear isometry equivalence expressing the associativity of the complete tensor + product of pairs of Hilbert spaces. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/CompleteTensorProduct.lean (CompleteTensorProduct.assoc) + + - description: + Proves that the complete tensor product is isometrically equivalent to the tensor product + when either factor is finite-dimensional. + done: false + location: N/A + + - description: + Defines the complete tensor product of an indexed family of Hilbert spaces. + done: false + location: N/A + + - description: + Defines the complete tensor power of a Hilbert space. + done: false + location: N/A + + - description: + Defines the Fock space of a seed Hilbert space. + done: false + location: N/A + + - description: + Defines Dirac notation for a general Hilbert space, scoped to a `DiracNotation` namespace. + done: false + location: N/A diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml index c356e0c08..7f1e97416 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -9,6 +9,7 @@ Overview: | ParentAPIs: - Space (Physlib/SpaceAndTime/Space) + - HilbertSpaces (Physlib/QuantumMechanics/HilbertSpaces) References: