From 5bd9c3d24df6f0b614557d65e5ca6ef9bcd8d484 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 12 Aug 2026 10:00:02 +0900 Subject: [PATCH 1/2] HS api map --- .../HilbertSpaces/API-map.yaml | 58 +++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 Physlib/QuantumMechanics/HilbertSpaces/API-map.yaml 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 From 064b80c6ee1da2d56a6a395717e5918bae258d21 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 12 Aug 2026 10:00:11 +0900 Subject: [PATCH 2/2] parent api --- Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml | 1 + 1 file changed, 1 insertion(+) 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: