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ⱼ.

TODO: Generalize to pinching with respect to arbitrary P(O)VM.

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_kraus_orthogonal {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {i j : ↑(spectrum ℝ ρ.m)} (h : i ≠ j) : ↑(pinching_kraus ρ i) * ↑(pinching_kraus ρ j) = 0

@[simp]

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

The Kraus operators of the pinching channelare projectors: they square to themselves.

theorem pinching_kraus_ortho {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (i j : ↑(spectrum ℝ ρ.m)) : ↑(pinching_kraus ρ i) * ↑(pinching_kraus ρ j) = if i = j then ↑(pinching_kraus ρ i) else 0

The Kraus operators of the pinching channel are orthogonal projectors.

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.mat ∘ pinching_kraus ρ) ⋯

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

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

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

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_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)

theorem ker_le_ker_pinching_of_PosDef {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (hpos : σ.m.PosDef) : (↑σ).ker ≤ (↑((pinching_map σ) ρ)).ker

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

theorem inner_cfc_pinching {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (f : ℝ → ℝ) : inner ℝ (↑ρ) ((↑((pinching_map σ) ρ)).cfc f) = inner ℝ (↑((pinching_map σ) ρ)) ((↑((pinching_map σ) ρ)).cfc f)

theorem inner_cfc_pinching_right {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (f : ℝ → ℝ) : inner ℝ (↑((pinching_map σ) ρ)) ((↑σ).cfc f) = inner ℝ (↑ρ) ((↑σ).cfc f)

theorem pinching_map_eq_sum_conj_hermitian {d : Type u_1} [Fintype d] [DecidableEq d] (σ ρ : MState d) : ↑((pinching_map σ) ρ) = ∑ k : ↑(spectrum ℝ σ.m), (HermitianMat.conj ↑(pinching_kraus σ k)) ↑ρ

theorem pinching_map_ker_le {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : (↑((pinching_map σ) ρ)).ker ≤ (↑ρ).ker

theorem pinching_kraus_ker_of_ne_zero {d : Type u_2} [Fintype d] [DecidableEq d] (σ : MState d) (v : d → ℂ) (hv : σ.m.mulVec v = 0) (k : ↑(spectrum ℝ σ.m)) (hk : ↑k ≠ 0) : (↑(pinching_kraus σ k)).mulVec v = 0

theorem ker_le_ker_pinching_map_ker {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (h : (↑σ).ker ≤ (↑ρ).ker) : (↑σ).ker ≤ (↑((pinching_map σ) ρ)).ker

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".