Canonical quantum channels

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

This file (phase C3 of specs/channels-plan.md) records the standard named channels as inhabitants of QuantumInfo.Channel:

• Channel.unitaryChannel U hU — a unitary channel ρ ↦ U ρ Uᴴ (a single Kraus operator U, Uᴴ U = 1). Generalises Channel.id (= unitaryChannel 1).
• Channel.traceOutChannel — the trace-out (partial-trace) channel ρ ↦ traceRight ρ on ℂ^(s ⊗ env), the literal "discard the environment". Obtained for free from the C2 Stinespring machinery as ofIsometry 1.
• Channel.mixedUnitaryChannel U hU p hp0 hp — a mixed-unitary (random-unitary) channel ρ ↦ ∑ᵢ pᵢ • (Uᵢ ρ Uᵢᴴ) for a probability vector p and unitaries Uᵢ, with Kraus operators √pᵢ • Uᵢ. This is the Cat-1-clean generalisation of the dephasing / depolarizing / bit-flip channels: each of those is mixedUnitaryChannel with a concrete Pauli family (assembled by the consumer, which supplies the Paulis — keeping this file Pauli-free).

The dephasing/depolarizing/bit-flip channels named in the plan are instances of mixedUnitaryChannel; the QEC error channel (phase C4) is the bit-flip instance.

Unitary channel

noncomputable def QuantumInfo.Channel.unitaryChannel {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℂ) (hU : U.conjTranspose * U = 1) : Channel n n PUnit.{u_2 + 1}

The unitary channel ρ ↦ U ρ Uᴴ of a unitary U (Uᴴ U = 1): a single Kraus operator. Generalises Channel.id (which is unitaryChannel 1).

Equations

• QuantumInfo.Channel.unitaryChannel U hU = { kraus := fun (x : PUnit.{?u.1 + 1}) => U, tp := ⋯ }

@[simp]

theorem QuantumInfo.Channel.unitaryChannel_apply {n : Type u_1} [Fintype n] [DecidableEq n] (U : Matrix n n ℂ) (hU : U.conjTranspose * U = 1) (ρ : Matrix n n ℂ) : (unitaryChannel U hU).apply ρ = U * ρ * U.conjTranspose

Trace-out channel

noncomputable def QuantumInfo.Channel.traceOutChannel (s : Type u_2) (env : Type u_3) [Fintype s] [Fintype env] [DecidableEq s] [DecidableEq env] : Channel (s × env) s env

The trace-out channel on ℂ^(s ⊗ env): discard the environment, ρ ↦ traceRight ρ. It is the C2 Stinespring channel of the identity isometry.

Equations

• QuantumInfo.Channel.traceOutChannel s env = QuantumInfo.Channel.ofIsometry 1 ⋯

@[simp]

theorem QuantumInfo.Channel.traceOutChannel_apply (s : Type u_2) (env : Type u_3) [Fintype s] [Fintype env] [DecidableEq s] [DecidableEq env] (ρ : Matrix (s × env) (s × env) ℂ) : (traceOutChannel s env).apply ρ = ρ.traceRight

Mixed-unitary (random-unitary) channel

theorem QuantumInfo.Channel.star_ofReal_sqrt {r : ℝ} : star ↑√r = ↑√r

Helper: star (√r : ℂ) = (√r : ℂ) (the square root is real).

theorem QuantumInfo.Channel.star_ofReal_sqrt_mul {r : ℝ} (hr : 0 ≤ r) : star ↑√r * ↑√r = ↑r

Helper: for r ≥ 0, star (√r : ℂ) * (√r : ℂ) = (r : ℂ).

noncomputable def QuantumInfo.Channel.mixedUnitaryChannel {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (U : ι → Matrix n n ℂ) (hU : ∀ (i : ι), (U i).conjTranspose * U i = 1) (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp : ∑ i : ι, p i = 1) : Channel n n ι

The mixed-unitary (random-unitary) channel ρ ↦ ∑ᵢ pᵢ • (Uᵢ ρ Uᵢᴴ): a convex combination (probabilities p, ∑ pᵢ = 1, pᵢ ≥ 0) of unitary conjugations, with Kraus operators √pᵢ • Uᵢ. The dephasing / depolarizing / bit-flip channels are the instances with a concrete Pauli family for U.

Equations

• QuantumInfo.Channel.mixedUnitaryChannel U hU p hp0 hp = { kraus := fun (i : ι) => ↑√(p i) • U i, tp := ⋯ }

@[simp]

theorem QuantumInfo.Channel.mixedUnitaryChannel_apply {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (U : ι → Matrix n n ℂ) (hU : ∀ (i : ι), (U i).conjTranspose * U i = 1) (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp : ∑ i : ι, p i = 1) (ρ : Matrix n n ℂ) : (mixedUnitaryChannel U hU p hp0 hp).apply ρ = ∑ i : ι, ↑(p i) • (U i * ρ * (U i).conjTranspose)

Local channel: Φ ⊗ id (Alice acts, Bob idle)

theorem QuantumInfo.Channel.sum_kronecker_one {p' : Type u_2} {n' : Type u_3} {ι' : Type u_4} [Fintype ι'] {b' : Type u_5} [DecidableEq b'] (f : ι' → Matrix p' n' ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (∑ i : ι', f i) 1 = ∑ i : ι', Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (f i) 1

Kronecker-with-identity commutes with finite sums on the left factor.

noncomputable def QuantumInfo.Channel.tensorRight {n : Type u_1} [Fintype n] [DecidableEq n] {p : Type u_2} {ι : Type u_3} [Fintype p] [Fintype ι] (Φ : Channel n p ι) (b : Type u_4) [Fintype b] [DecidableEq b] : Channel (n × b) (p × b) ι

The local channel Φ ⊗ id_b: Alice applies the channel Φ to her factor while Bob's factor b is left idle. Kraus operators Φ.kraus i ⊗ I_b.

Equations

• Φ.tensorRight b = { kraus := fun (i : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Φ.kraus i) 1, tp := ⋯ }

@[simp]

theorem QuantumInfo.Channel.tensorRight_apply {n : Type u_1} [Fintype n] [DecidableEq n] {p : Type u_2} {ι : Type u_3} [Fintype p] [Fintype ι] (Φ : Channel n p ι) (b : Type u_4) [Fintype b] [DecidableEq b] (ρ : Matrix (n × b) (n × b) ℂ) : (Φ.tensorRight b).apply ρ = ∑ i : ι, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Φ.kraus i) 1 * ρ * (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Φ.kraus i) 1).conjTranspose

theorem QuantumInfo.Channel.tensorRight_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {p : Type u_2} {ι : Type u_3} [Fintype p] [Fintype ι] (Φ : Channel n p ι) (b : Type u_4) [Fintype b] [DecidableEq b] {ρ : Matrix (n × b) (n × b) ℂ} (hρ : ρ.PosSemidef) : ((Φ.tensorRight b).apply ρ).PosSemidef

Complete positivity, witnessed. For every idle factor b, the local channel Φ ⊗ id_b maps positive-semidefinite operators to positive-semidefinite operators — the formal CP statement the Kraus form justifies, immediate because tensorRight is itself a Channel and every channel's action is positive (apply_posSemidef).