Skip to content

feat(QuantumMechanics): Add TODO item for QM #1084

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jstoobysmith wants to merge 2 commits into
base: master
Choose a base branch
from
+17 −0
Open

feat(QuantumMechanics): Add TODO item for QM #1084

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7701550
feat(QuantumMechanics): Add TODO item for QM
jstoobysmith May 6, 2026
ad853a6
refactor: Fix import
jstoobysmith May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions Physlib/QuantumMechanics/FiniteTarget/HilbertSpace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
module

public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Physlib.Meta.TODO.Basic
/-!

# The Hilbert space of a finite target quantum mechanical system
Expand All @@ -16,6 +17,22 @@ public import Mathlib.Analysis.InnerProductSpace.PiL2

namespace QuantumMechanics

TODO "To match this with the results currently in the `QuantumInfo` part of the library,
we should:
1. Define `FiniteHilbertSpace` as a structure with a single entry `val`, this
should take as an input a finite and decidable type `d`. Below this type is
taken as default to be `Fin n`.
2. On this type we should then define the structure of an inner-product space, and a
Hilbert space.
3. We could then define the notation `𝓗[d]` to denote the Hilbert space corresponding
to the type `d`.
4. The results from `QuantumInfo/Finite/Braket.lean` can then be moved over
to Physlib, and related to the definition of the Hilbert space here.
Optional. Maybe it is worth moving these files to a directory called `States`, with
the idea that it includes this definition of the Hilbert space, the
definition of bras and kets, and the definition of mixed states. Maybe also
parts of `./ResourceTheory/FreeState`."

/-- The finite dimensional Hilbert space of dimension `n`. -/
def FiniteHilbertSpace (n : ℕ) : Type := EuclideanSpace ℂ (Fin n)

Expand Down
Loading