Quantum error correction

Quantum error correction codes protect information passing through noisy Quantum channels. For example: A stabilizer code achieves the hashing bound as a rate for quantum communication using Pauli channels;

• Quantum codes satisfy certain properties;

/-- An isometry from ℋ₂ᵏ to ℋ₂ⁿ -/
structure quantum_code : Type :=
(k : ℕ)
(n : ℕ)
(isometry : ℋ₂ᵏ →ₗ[C] ℋ₂ⁿ)

/-
"Alternatively: A unitary from ℋ₂ᵏ ⊗ ℋ₂ⁿ⁻ᵏ to ℋ₂ⁿ,
where the Quantum state in ℋ₂ⁿ⁻ᵏ is |0〉."

Or

"A unitary map from ℋ₂ᵏ to a 2ᵏ-dimensional subspace of ℋ₂ⁿ."
-/

def quantum_code_rate (Q : quantum_code) : ℝ := 
Q.k / Q.n

• Is Quantum error correction the same as Reversing quantum channels?;

• Approximate quantum error correction;

References

• Shor1996;