Primitive Quantum Channels

This file contains basic formalization toward the theory of primitive quantum channels (Wolf Section 6.3, Theorem 6.7: equivalent characterizations of primitivity).

We formalize the rank-one projection onto a fixed point and the algebraic decomposition [ E^n = P + (E-P)^n \qquad (n \ge 1) ] where P is the fixed-point projection. This decomposition is the algebraic core of Wolf Theorem 6.7 item 3 → item 1: a complementary transfer-map gap for E - P ensures (E - P)^n → 0, so E^n → P, giving convergence to the unique fixed state.

Main definitions

• fixedPointProj: rank-one projection X ↦ (tr X / tr ρ) • ρ onto a fixed state ρ

Main results

• fixedPointProj_idempotent: P ∘ P = P
• pow_succ_eq_fixedPointProj_add_compl_pow: E^(n+1) = P + (E-P)^(n+1) for all n
• pow_eq_fixedPointProj_add_compl_pow: same for all n ≥ 1
• LinearMap.trace_pow_tendsto_one_of_spectralRadius_compl_lt_one: convergence of the traces to one under a complementary spectral-radius gap

Notation

Within section ComplementaryDecomposition, we use local notation:

• P for fixedPointProj ρ htr
• N for E - P (the complementary part)

References

• [M. Wolf, Quantum Channels & Operations: Guided Tour, Section 6.3 Theorem 6.7][Wolf2012QChannels]

noncomputable def fixedPointProj {D : ℕ} (ρ : Matrix (Fin D) (Fin D) ℂ) (_htr : ρ.trace ≠ 0) : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ

The rank-one projection onto ρ, normalized by trace ρ.

We keep the hypothesis trace ρ ≠ 0 as a parameter so later lemmas can use it to cancel denominators.

Equations

• fixedPointProj ρ _htr = { toFun := fun (X : Matrix (Fin D) (Fin D) ℂ) => (X.trace / ρ.trace) • ρ, map_add' := ⋯, map_smul' := ⋯ }

theorem fixedPointProj_idempotent {D : ℕ} (ρ : Matrix (Fin D) (Fin D) ℂ) (htr : ρ.trace ≠ 0) (X : Matrix (Fin D) (Fin D) ℂ) : (fixedPointProj ρ htr) ((fixedPointProj ρ htr) X) = (fixedPointProj ρ htr) X

The fixed-point projection is idempotent.

theorem fixedPointProj_trace {D : ℕ} (ρ : Matrix (Fin D) (Fin D) ℂ) (htr : ρ.trace ≠ 0) : (LinearMap.trace ℂ (Matrix (Fin D) (Fin D) ℂ)) (fixedPointProj ρ htr) = 1

The trace of fixedPointProj ρ as a linear endomorphism is 1.

The proof expresses fixedPointProj ρ htr as the rank-one map X ↦ f(X) • ρ for f := (trace ρ)⁻¹ • traceLinearMap, then applies the rank-one trace formula.

theorem fixedPointProj_mul_self {D : ℕ} {ρ : Matrix (Fin D) (Fin D) ℂ} (htr : ρ.trace ≠ 0) : fixedPointProj ρ htr * fixedPointProj ρ htr = fixedPointProj ρ htr

The fixed-point projection is idempotent as an endomorphism: P * P = P.

theorem pow_succ_eq_fixedPointProj_add_compl_pow {D : ℕ} (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ) {ρ : Matrix (Fin D) (Fin D) ℂ} (htr : ρ.trace ≠ 0) (hTP : IsTracePreservingMap E) (hρ : E ρ = ρ) (n : ℕ) : E ^ (n + 1) = fixedPointProj ρ htr + (E - fixedPointProj ρ htr) ^ (n + 1)

For P := fixedPointProj ρ and N := E - P, we have E^(n+1) = P + N^(n+1).

This is the algebraic core of primitive convergence: the dynamics splits into the fixed-point part P and a complementary part N that decays under a complementary transfer-map gap hypothesis.

theorem pow_eq_fixedPointProj_add_compl_pow {D : ℕ} (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ) {ρ : Matrix (Fin D) (Fin D) ℂ} (htr : ρ.trace ≠ 0) (hTP : IsTracePreservingMap E) (hρ : E ρ = ρ) {n : ℕ} (hn : 1 ≤ n) : E ^ n = fixedPointProj ρ htr + (E - fixedPointProj ρ htr) ^ n

For P := fixedPointProj ρ and N := E - P, we have E^n = P + N^n for all n ≥ 1.

theorem LinearMap.trace_pow_tendsto_one_of_spectralRadius_compl_lt_one {D : ℕ} [NeZero D] (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ) (ρ : Matrix (Fin D) (Fin D) ℂ) (htr : ρ.trace ≠ 0) (hTP : IsTracePreservingMap E) (hρ : E ρ = ρ) (hSpect : spectralRadius ℂ ((Module.End.toContinuousLinearMap (Matrix (Fin D) (Fin D) ℂ)) (E - fixedPointProj ρ htr)) < 1) : Filter.Tendsto (fun (n : ℕ) => (trace ℂ (Matrix (Fin D) (Fin D) ℂ)) (E ^ n)) Filter.atTop (nhds 1)

Let P be the rank-one projection onto a fixed point ρ and let N := E - P. If the spectral radius of N is less than one, then trace(E ^ n) converges to one.