Quantum instrument
input : Quantum state output: a quantum system and a classical system
A Quantum instrument: Apply a mixture of Quantum channels chosen according to a probability distribution that depends on input state ρ.
“use quantum instrument when require device that outputs both a classical and quantum system.”
class quantum_instrument (ℰ : ι → {ℰᵢ | completely_positive ℰᵢ ∧ trace_non_increasing ℰᵢ}) :=
(sum_map_trace_preserving : trace_preserving ∑ i, (ℰ i))
Let {|j⟩} be an orthonormal basis for a Hilbert space ℋJ.
The action of a Quantum instrument on a Quantum state ρ is the following Quantum channel, which features a quantum and classical output:
def quantum_instrument_map [quantum_instrument ℰ] [quantum_state ρ] := λ ρ, ∑ j, (ℰ j)(ρ) ⊗ |j⟩⟨j| lemma cp_quantum_instrument_map : completely_pos quantum_instrument_map ℰ := sorry lemma tp_quantum_instrument_map : trace_preserving quantum_instrument_map ℰ := sorry instance quantum_channel_quantum_instrument_map : quantum_channel quantum_instrument_map ℰ := ⟨cp_quantum_instrument_map, tp_quantum_instrument_map⟩
Tr{∑ j, (ℰ j)(ρ)} = ∑ j, Tr{(ℰ j)(ρ)} = ∑ j, p ρ j = 1
/--
Equivalent to the definition above?
-/
def apply_quantum_instrument [quantum_state ρ] (ℰ : ι → {ℰᵢ | quantum_channel ℰᵢ}) :=
∑ j, (p ρ j) * (ℰ j)(ρ) ⊗ |j⟩⟨j|
The number of terms in the mixture is equal to the cardinality of the set {|j⟩}, orthonormal basis for Hilbert space ℋJ.
We can measure the classical output system to determine which channel was applied.