Stinespring dilation

theorem stinespringForm_eq {R : Type u_1} [RCLike R] {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) R) (ρ : Matrix (Fin m) (Fin m) R) : tr₂ (stinespringDilation K ρ) = krausApply K ρ

A version of the Stinespring Dilation Theorem.

theorem heisenberg_schrõdinger_picture {m r : ℕ} (K : Fin r.succ → Matrix (Fin m) (Fin m) ℂ) (ρ : Matrix (Fin m) (Fin m) ℂ) : 0 = 0

theorem tr₂_one_of_unital {m r : ℕ} (K : Fin r → Matrix (Fin m) (Fin m) ℂ) (hu : unital K) : tr₂ (stinespringOp K * (stinespringOp K).conjTranspose) = 1