Finite dimensional quantum pure states, bra and kets. Mixed states are MState in that file.

These could be done with a Hilbert space of Fintype, which would look like

(H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H]

or by choosing a particular Basis and asserting it is Fintype. But frankly it seems easier to mostly focus on the basis-dependent notion of Matrix, which has the added benefit of an obvious "classical" interpretation (as the basis elements, or diagonal elements of a mixed state). In that sense, this quantum theory comes with the a particular classical theory always preferred.

structure Ket (d : Type u_1) [Fintype d] : Type u_1

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.

• vec : d → ℂ
• normalized' : ∑ x : d, ‖self.vec x‖ ^ 2 = 1

structure Bra (d : Type u_1) [Fintype d] : Type u_1

A bra is identical in definition to a Ket, but are separate to avoid complex conjugation confusion. They can be interconverted with the adjoint: Ket.to_bra and Bra.to_ket

• vec : d → ℂ
• normalized' : ∑ x : d, ‖self.vec x‖ ^ 2 = 1

def Braket.«term〈_∣» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Braket.«term∣_〉» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance Braket.instFunLikeKet {d : Type u_1} [Fintype d] : FunLike (Ket d) d ℂ

Equations

• Braket.instFunLikeKet = { coe := fun (ψ : Ket d) => ψ.vec, coe_injective' := ⋯ }

instance Braket.instFunLikeBra {d : Type u_1} [Fintype d] : FunLike (Bra d) d ℂ

Equations

• Braket.instFunLikeBra = { coe := fun (ψ : Bra d) => ψ.vec, coe_injective' := ⋯ }

def Braket.dot {d : Type u_1} [Fintype d] (ξ : Bra d) (ψ : Ket d) : ℂ

Equations

• Braket.dot ξ ψ = ∑ x : d, ξ x * ψ x

def Braket.«term〈_‖_〉» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Braket.dot_eq_dotProduct {d : Type u_1} [Fintype d] (ψ : Bra d) (φ : Ket d) : dot ψ φ = ⇑ψ ⬝ᵥ ⇑φ

theorem Ket.apply {d : Type u_1} [Fintype d] (ψ : Ket d) (i : d) : ψ i = ψ.vec i

theorem Bra.apply {d : Type u_1} [Fintype d] (ψ : Bra d) (i : d) : ψ i = ψ.vec i

theorem Ket.ext {d : Type u_1} [Fintype d] {ξ ψ : Ket d} (h : ∀ (x : d), ξ x = ψ x) : ξ = ψ

theorem Ket.ext_iff {d : Type u_1} [Fintype d] {ξ ψ : Ket d} : ξ = ψ ↔ ∀ (x : d), ξ x = ψ x

theorem Bra.ext {d : Type u_1} [Fintype d] {ξ ψ : Bra d} (h : ∀ (x : d), ξ x = ψ x) : ξ = ψ

theorem Bra.ext_iff {d : Type u_1} [Fintype d] {ξ ψ : Bra d} : ξ = ψ ↔ ∀ (x : d), ξ x = ψ x

theorem Ket.normalized {d : Type u_1} [Fintype d] (ψ : Ket d) : ∑ x : d, Complex.normSq (ψ x) = 1

theorem Bra.normalized {d : Type u_1} [Fintype d] (ψ : Bra d) : ∑ x : d, Complex.normSq (ψ x) = 1

def Ket.to_bra {d : Type u_1} [Fintype d] (ψ : Ket d) : Bra d

Any Bra can be turned into a Ket by conjugating the elements.

Equations

• ↑ψ = { vec := (starRingEnd (d → ℂ)) ⇑ψ, normalized' := ⋯ }

def Bra.to_ket {d : Type u_1} [Fintype d] (ψ : Bra d) : Ket d

Any Ket can be turned into a Bra by conjugating the elements.

Equations

• ↑ψ = { vec := (starRingEnd (d → ℂ)) ⇑ψ, normalized' := ⋯ }

instance instBraOfKet {d : Type u_1} [Fintype d] : Coe (Ket d) (Bra d)

Equations

• instBraOfKet = { coe := Ket.to_bra }

instance instKetOfBra {d : Type u_1} [Fintype d] : Coe (Bra d) (Ket d)

Equations

• instKetOfBra = { coe := Bra.to_ket }

@[simp]

theorem Bra.eq_conj {d : Type u_1} [Fintype d] (ψ : Ket d) (x : d) : ↑ψ x = (starRingEnd ℂ) (ψ x)

theorem Bra.apply' {d : Type u_1} [Fintype d] (ψ : Ket d) (i : d) : ↑ψ i = (starRingEnd ℂ) (ψ.vec i)

theorem Ket.exists_ne_zero {d : Type u_1} [Fintype d] (ψ : Ket d) : ∃ (x : d), ψ x ≠ 0

theorem Bra.exists_ne_zero {d : Type u_1} [Fintype d] (ψ : Bra d) : ∃ (x : d), ψ x ≠ 0

def Ket.normalize {d : Type u_1} [Fintype d] (v : d → ℂ) (h : ∃ (x : d), v x ≠ 0) : Ket d

Create a ket out of a vector given it has a nonzero component

Equations

• Ket.normalize v h = { vec := fun (x : d) => v x / ↑√(∑ x : d, ‖v x‖ ^ 2), normalized' := ⋯ }

theorem Ket.normalize_ket_eq_self {d : Type u_1} [Fintype d] (ψ : Ket d) : normalize ψ.vec ⋯ = ψ

A ket is already normalized

def Bra.normalize {d : Type u_1} [Fintype d] (v : d → ℂ) (h : ∃ (x : d), v x ≠ 0) : Bra d

Create a bra out of a vector given it has a nonzero component

Equations

• Bra.normalize v h = { vec := fun (x : d) => v x / ↑√(∑ x : d, ‖v x‖ ^ 2), normalized' := ⋯ }

def Bra.normalize_ket_eq_self {d : Type u_1} [Fintype d] (ψ : Bra d) : normalize ψ.vec ⋯ = ψ

A bra is already normalized

Equations

• ⋯ = ⋯

def uniform_superposition {d : Type u_1} [Fintype d] [hdne : Nonempty d] : Ket d

Ket form by the superposition of all elements in d. Commonly denoted by |+⟩, especially for qubits

Equations

• uniform_superposition = Ket.normalize (fun (x : d) => 1) ⋯

instance instInhabited {d : Type u_1} [Fintype d] [Nonempty d] : Inhabited (Ket d)

There exists a ket for every nonempty d. Here, we use the uniform superposition

Equations

• instInhabited = { default := uniform_superposition }

def Ket.basis {d : Type u_1} [Fintype d] (i : d) : Ket d

Construct the Ket corresponding to a basis vector, with a +1 phase.

Equations

• Ket.basis i = { vec := fun (j : d) => if i = j then 1 else 0, normalized' := ⋯ }

def Bra.basis {d : Type u_1} [Fintype d] (i : d) : Bra d

Construct the Bra corresponding to a basis vector, with a +1 phase.

Equations

• Bra.basis i = { vec := fun (j : d) => if i = j then 1 else 0, normalized' := ⋯ }

instance instFunLikeBraket {d : Type u_1} [Fintype d] : FunLike (Bra d) (Ket d) ℂ

A Bra can be viewed as a function from Ket's to ℂ.

Equations

• instFunLikeBraket = { coe := fun (ξ : Bra d) => Braket.dot ξ, coe_injective' := ⋯ }

@[simp]

theorem Braket.dot_self_eq_one {d : Type u_1} [Fintype d] (ψ : Ket d) : dot (↑ψ) ψ = 1

The inner product of any state with itself is 1.

def Ket.prod {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ₁ : Ket d₁) (ψ₂ : Ket d₂) : Ket (d₁ × d₂)

The outer product of two kets, creating an unentangled state.

Equations

• ψ₁ ⊗ ψ₂ = { vec := fun (x : d₁ × d₂) => match x with | (i, j) => ψ₁ i * ψ₂ j, normalized' := ⋯ }

def «term_⊗_» : Lean.TrailingParserDescr

Equations

• «term_⊗_» = Lean.ParserDescr.trailingNode `«term_⊗_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 101))

def Ket.IsProd {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ : Ket (d₁ × d₂)) : Prop

A Ket is a product if it's Ket.prod of two kets.

Equations

• ψ.IsProd = ∃ (ξ : Ket d₁) (φ : Ket d₂), ψ = ξ ⊗ φ

def Ket.IsEntangled {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ : Ket (d₁ × d₂)) : Prop

A Ket is entangled if it's not Ket.prod of two kets.

Equations

• ψ.IsEntangled = ¬ψ.IsProd

@[simp]

theorem Ket.IsProd_prod {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ₁ : Ket d₁) (ψ₂ : Ket d₂) : (ψ₁ ⊗ ψ₂).IsProd

Ket.prod states are product states.

@[simp]

theorem Ket.not_IsEntangled_prod {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ₁ : Ket d₁) (ψ₂ : Ket d₂) : ¬(ψ₁ ⊗ ψ₂).IsEntangled

Ket.prod states are not entangled states.

theorem Ket.IsProd_iff_mul_eq_mul {d₁ : Type u_3} {d₂ : Type u_4} [Fintype d₁] [Fintype d₂] (ψ : Ket (d₁ × d₂)) : ψ.IsProd ↔ ∀ (i₁ i₂ : d₁) (j₁ j₂ : d₂), ψ (i₁, j₁) * ψ (i₂, j₂) = ψ (i₁, j₂) * ψ (i₂, j₁)

A ket is a product state iff its components are cross-multiplicative.

def Ket.MES (d : Type u_2) [Fintype d] [Nonempty d] : Ket (d × d)

The Maximally Entangled State, or MES, on a d×d system. In principle there are many, this is specifically the MES with an all-positive phase. For instance on d := Fin 2, this is the Bell state.

Equations

• Ket.MES d = { vec := fun (x : d × d) => match x with | (i, j) => if i = j then 1 / ↑√↑(Fintype.card d) else 0, normalized' := ⋯ }

theorem Ket.MES_isEntangled {d : Type u_1} [Fintype d] [Nontrivial d] : (MES d).IsEntangled

On any space of dimension at least two, the maximally entangled state MES is entangled.

theorem TransposeTrick {d : Type u_2} [Fintype d] [Nonempty d] [DecidableEq d] {M : Matrix d d ℂ} : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1).mulVec (Ket.MES d).vec = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M.transpose).mulVec (Ket.MES d).vec

The transpose trick

def Ket.PhaseEquiv {d : Type u_1} [Fintype d] : Setoid (Ket d)

The equivalence relation on Ket where two kets equivalent if they are equal up to a global phase, i.e. `∃ z, ‖z‖ = 1 ∧ a.vec = z • b.vec

Equations

• Ket.PhaseEquiv = { r := fun (a b : Ket d) => ∃ (z : ℂ), ‖z‖ = 1 ∧ a.vec = z • b.vec, iseqv := ⋯ }

def KetUpToPhase (d : Type u_1) [Fintype d] : Type u_1

The type of Kets up to a global phase equivalence, as given by Ket.PhaseEquiv. In particular, MStates really only care about a KetUpToPhase, and not Kets themselves.

Equations

• KetUpToPhase d = Quotient Ket.PhaseEquiv