Definition of HilbertSpace

[teng10]

Hello,

I'm a new contributor to lean and saw the project on UnitaryHack, I didnt see explicit projects there so I looked over existing issues and decided to work on the definition of HilbertSpace to start. This PR makes progress towards the issue
I have tried to follow the TODO instructions in QuantumMechanics\HilbertSpace.lean.

Summary of changes

• Added a FiniteHilbertSpace structure as EuclideanSpace carrying a val etnry as suggested in the TODO.
  • Because we are defining a structure, we need to use equivEuclideanto transfer AddCommGroupand Module properties for a vector space.
• The rest of the files are to carry over properties of a Hilbert space , as we need the definition to have the following properties such that it is compatible with QuantumInfo/Finite/Braket.lean.
  (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H]
• The linearEquivEuclidean definition transfers NormedAddCommGroup, InnerProductSpace, CompleteSpaceand FiniteDimensional.
• Finally to make this defintiion compatible to TightBindingChain/Basic.lean , we also define basisFun.

AI usage
As a beginner in writing lean code, I have used claude code and instructed the writing to be as close to mathlib quality. I have interacted with the AI for multiple sessions and have read all the lines of the code and tried to have a high level understanding as mentioned above. However, I realize I probably am not able to fully understand the nuance of design decisions and would very much appreciate your feedback on these.

The modfied files compile in lean, my linter passed 1/7 but is currently taking a very long time on step 2, if its ok I can come back to the linter.
Additionallz I have followed the review guidelines but could have missed something. Look forward to your feedback.

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[teng10]

For reference, I kept the old definition here as comments

[jstoobysmith]

This looks like a great first PR. Only one comment from me which is: Feel free to remove the old stuff - it is saved in the git history, so we can always retrieve it if need be.

I've added an awaiting-author label, when this is done could you comment with a comment that says -awaiting-author (this will remove this label).

[teng10]

Ok thanks for the feedback! I removed the commented code

[teng10]

-awaiting-author

[jstoobysmith]

Approved! Will merge shortly