Composition of quantum channels

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Channel.comp Ψ Φ is the composite channel with Kraus family {Ψₐ Φₖ} indexed by κ × ι; the trace-preserving constraint follows by inserting ∑ₐ Ψₐᴴ Ψₐ = 1 into ∑ₖ Φₖᴴ (·) Φₖ, and comp_apply says the action composes. Index-generic; the Fin-indexed CSD.LF2.QuantumChannel.comp maps to this composition under CSD.LF2.QuantumChannel.toChannel (LF2/ChannelBridge.lean).

Composition of QuantumInfo.Channel (index-generic)

noncomputable def QuantumInfo.Channel.comp {n : Type u_1} {m : Type u_2} {p : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype n] [Fintype m] [Fintype p] [Fintype ι] [Fintype κ] [DecidableEq n] [DecidableEq m] (Ψ : Channel m p κ) (Φ : Channel n m ι) : Channel n p (κ × ι)

Channels compose: the composite Ψ ∘ Φ has Kraus family {Ψₐ Φₖ} indexed by κ × ι.

Equations

• Ψ.comp Φ = { kraus := fun (q : κ × ι) => Ψ.kraus q.1 * Φ.kraus q.2, tp := ⋯ }

@[simp]

theorem QuantumInfo.Channel.comp_kraus {n : Type u_1} {m : Type u_2} {p : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype n] [Fintype m] [Fintype p] [Fintype ι] [Fintype κ] [DecidableEq n] [DecidableEq m] (Ψ : Channel m p κ) (Φ : Channel n m ι) (q : κ × ι) : (Ψ.comp Φ).kraus q = Ψ.kraus q.1 * Φ.kraus q.2

theorem QuantumInfo.Channel.comp_apply {n : Type u_1} {m : Type u_2} {p : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype n] [Fintype m] [Fintype p] [Fintype ι] [Fintype κ] [DecidableEq n] [DecidableEq m] (Ψ : Channel m p κ) (Φ : Channel n m ι) (ρ : Matrix n n ℂ) : (Ψ.comp Φ).apply ρ = Ψ.apply (Φ.apply ρ)

The composite acts by composing the actions.