Skip to content

Questions about definition of a KET #18

@swiswioo24

Description

@swiswioo24

I have a question about this definition part.

/-- A ket as a vector of unit norm. We follow the convention in `Matrix` of vectors as simple functions
 from a Fintype. Kets are distinctly not a vector space in our notion, as they represent only normalized
 states and so cannot (in general) be added or scaled. -/
structure Ket where
  vec : d → ℂ
  normalized' : ∑ x, ‖vec x‖ ^ 2 = 1
  --TODO: change to `vec : EuclideanSpace ℂ d` / `normalized' : ‖vec‖ = 1`

My question is, what are the pros and cons of using this definition?

May I simply use a $$2n \times 1$$ matrix to represent a ket and force the 'norm' to be 1? Or at least use a vector of dimension $2n$ and normalize it?

Metadata

Metadata

Assignees

No one assigned

    Labels

    questionFurther information is requested

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions