Pinching channels

A pinching channel decoheres in the eigenspaces of a given state. More precisely, given a state ρ, the pinching channel with respect to ρ is defined as E(σ) = ∑ Pᵢ σ Pᵢ where the P_i are the projectors onto the i-th eigenspaces of ρ = ∑ᵢ pᵢ Pᵢ, with i ≠ j → pᵢ ≠ pⱼ.

def pinching_kraus {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ↑(spectrum ℝ ρ.m) → HermitianMat d ℂ

Equations

• pinching_kraus ρ x = (↑ρ).cfc fun (y : ℝ) => if y = ↑x then 1 else 0

theorem pinching_kraus_commutes {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (i : ↑(spectrum ℝ ρ.m)) : Commute (↑(pinching_kraus ρ i)) ρ.m

theorem pinching_kraus_mul_self {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (i : ↑(spectrum ℝ ρ.m)) : ↑(pinching_kraus ρ i) * ρ.m = ↑i • ↑(pinching_kraus ρ i)

instance finite_spectrum_inst {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Fintype ↑(spectrum ℝ ρ.m)

Equations

• finite_spectrum_inst ρ = Fintype.ofFinite ↑(spectrum ℝ ρ.m)

theorem pinching_sq_eq_self {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (k : ↑(spectrum ℝ ρ.m)) : pinching_kraus ρ k ^ 2 = pinching_kraus ρ k

theorem pinching_sum {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ∑ k : ↑(spectrum ℝ ρ.m), pinching_kraus ρ k = 1

def pinching_map {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : CPTPMap d d ℂ

Equations

• pinching_map ρ = CPTPMap.of_kraus_CPTPMap (HermitianMat.toMat ∘ pinching_kraus ρ) ⋯

theorem pinchingMap_apply_M {d : Type u_1} [Fintype d] [DecidableEq d] (σ ρ : MState d) : ↑((pinching_map σ) ρ) = ⟨(MatrixMap.of_kraus (HermitianMat.toMat ∘ pinching_kraus σ) (HermitianMat.toMat ∘ pinching_kraus σ)) ↑↑ρ, ⋯⟩

theorem pinching_commutes {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : Commute ((pinching_map σ) ρ).m σ.m

@[simp]

theorem pinching_self {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : (pinching_map ρ) ρ = ρ

theorem pinching_pythagoras {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : 𝐃(ρ‖σ) = 𝐃(ρ‖(pinching_map σ) ρ) + 𝐃((pinching_map σ) ρ‖σ)

Exercise 2.8 of Hayashi's book "A group theoretic approach to Quantum Information". -- Used in (S59)

theorem HermitianMat.le_iff_mulVec_le_mulVec {d : Type u_1} [Fintype d] {𝕜 : Type u_2} [RCLike 𝕜] (A B : HermitianMat d 𝕜) : A ≤ B ↔ ∀ (v : d → 𝕜), star v ⬝ᵥ (↑A).mulVec v ≤ star v ⬝ᵥ (↑B).mulVec v

theorem pinching_bound {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ↑ρ ≤ ↑(Fintype.card ↑(spectrum ℝ σ.m)) • ↑((pinching_map σ) ρ)

Lemma 3.10 of Hayashi's book "Quantum Information Theory - Mathematical Foundations". Also, Lemma 5 in https://arxiv.org/pdf/quant-ph/0107004. -- Used in (S60)