Quantum channel

/--
A Quantum channel is a linear map 
between two linear operators 
on complex hilbert spaces ℋ₁ and ℋ₂.
-/
class quantum_channel (𝒩 : (ℋ₁ →ₗ[ℂ] ℋ₁) →ₗ[ℂ] (ℋ₂ →ₗ[ℂ] ℋ₂)) :=
(completely_positive : completely_positive 𝒩)
(trace_preserving    : ∀ (ρ : ℋ₁ →ₗ[ℂ] ℋ₁), Tr(𝒩 ρ) = Tr(ρ))

A Quantum channel can be used to model the passage of a quantum system through a process.

⇅ ============ ⇅

𓂻

For example: A Quantum computing process.

Quantum channels are generally noisy. Quantum error correction protects information as it passes through. Try to achieve the channel’s Capacity for quantum communication;

• Capacity for classical communication;

• Capacity for private classical communication;

/-- quantum channel 𝒩 can be written as unitary on input and environment -/
theorem unitary_on_input_and_environment_of_channel {quantum_channel 𝒩} :
  ∃ U, Tr_env{U ρ⊗|0⟩_env U†} = 𝒩(ρ) :=
sorry

References

• Wilde2011;