Dimension 3

e₁ etc.

def e₁ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₁ = ![1, 0, 0]

def e₂ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₂ = ![0, 1, 0]

def e₃ {R : Type u_1} [One R] [Zero R] : Matrix (Fin 3) (Fin 1) R

Equations

• e₃ = ![0, 0, 1]

theorem pureState_probability_one {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hρ : ρ.trace = 1) : (pureState e₁ * ρ).trace + (pureState e₂ * ρ).trace + (pureState e₃ * ρ).trace = 1

The positive operator pureState e₁ is chosen with probability (pureState e₁ * ρ).trace.

theorem pureState_probability_one_C {R : Type u_1} [RCLike R] {ρ : Matrix (Fin 3) (Fin 3) R} (hρ : ρ.trace = 1) : (pureState_C e₁ * ρ).trace + (pureState_C e₂ * ρ).trace + (pureState_C e₃ * ρ).trace = 1