KrausChannels.lean

1 module
2 public import Mathlib.LinearAlgebra.Matrix.PosDef
3 public import Mathlib.LinearAlgebra.Matrix.Kronecker
4 public import Mathlib.LinearAlgebra.Matrix.Trace
5 public import Mathlib.Analysis.Complex.Basic
6 /-! Author: Komorebi P. Paper VII second block, Classical input 7.2.
7 Actual block amplification identified with identity-tensor Kraus operators. -/
8 public section
9 set_option autoImplicit false
10 namespace KomorebiPaperVII.Kraus
11 open scoped BigOperators Kronecker ComplexOrder
12 variable {n A : Type*} [Fintype n] [Fintype A]
13 def channel (K : A → Matrix n n ℂ) (rho : Matrix n n ℂ) : Matrix n n ℂ :=
14   ∑ a, K a * rho * (K a).conjTranspose
15 
16 theorem channel_add (K : A → Matrix n n ℂ) (rho sigma : Matrix n n ℂ) :
17     channel K (rho + sigma) = channel K rho + channel K sigma := by
18   simp [channel, Matrix.mul_add, Matrix.add_mul, Finset.sum_add_distrib]
19 
20 theorem channel_smul (K : A → Matrix n n ℂ) (c : ℂ) (rho : Matrix n n ℂ) :
21     channel K (c • rho) = c • channel K rho := by
22   simp [channel, Finset.smul_sum]
23 
24 def linearMap (K : A → Matrix n n ℂ) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ where
25   toFun := channel K
26   map_add' := channel_add K
27   map_smul' := channel_smul K
28 
29 theorem channel_positive (K : A → Matrix n n ℂ) {rho : Matrix n n ℂ}
30     (hrho : rho.PosSemidef) : (channel K rho).PosSemidef := by
31   exact Matrix.posSemidef_sum _ (fun a _ => hrho.mul_mul_conjTranspose_same (K a))
32 
33 theorem channel_trace_preserving [DecidableEq n] (K : A → Matrix n n ℂ)
34     (hK : ∑ a, (K a).conjTranspose * K a = 1) (rho : Matrix n n ℂ) :
35     Matrix.trace (channel K rho) = Matrix.trace rho := by
36   unfold channel
37   rw [Matrix.trace_sum]
38   have cyclic (a : A) : Matrix.trace (K a * rho * (K a).conjTranspose) =
39       Matrix.trace (((K a).conjTranspose * K a) * rho) := by
40     rw [Matrix.trace_mul_comm, Matrix.mul_assoc]
41   simp_rw [cyclic]
42   rw [← Matrix.trace_sum, ← Finset.sum_mul, hK, Matrix.one_mul]
43 
44 def amplify {J : Type*} (Phi : Matrix n n ℂ → Matrix n n ℂ)
45     (rho : Matrix (J × n) (J × n) ℂ) : Matrix (J × n) (J × n) ℂ :=
46   fun x y => Phi (fun u v => rho (x.1, u) (y.1, v)) x.2 y.2
47 
48 theorem amplification_eq_kraus {J : Type*} [Fintype J] [DecidableEq J]
49     (K : A → Matrix n n ℂ) (rho : Matrix (J × n) (J × n) ℂ) :
50     amplify (channel K) rho =
51       channel (fun a => (1 : Matrix J J ℂ) ⊗ₖ K a) rho := by
52   ext ⟨i, u⟩ ⟨j, v⟩
53   simp_rw [amplify, channel, Matrix.sum_apply, Matrix.mul_apply,
54     Matrix.conjTranspose_apply, Matrix.kroneckerMap_apply]
55   simp [Fintype.sum_prod_type, Matrix.one_apply, apply_ite]
56   rfl
57 
58 theorem channel_completely_positive {J : Type*} [Fintype J] [DecidableEq J]
59     (K : A → Matrix n n ℂ) {rho : Matrix (J × n) (J × n) ℂ}
60     (hrho : rho.PosSemidef) : (amplify (channel K) rho).PosSemidef := by
61   rw [amplification_eq_kraus]
62   exact channel_positive _ hrho
63 
64 theorem channel_density_matrix [DecidableEq n] (K : A → Matrix n n ℂ)
65     (hK : ∑ a, (K a).conjTranspose * K a = 1) {rho : Matrix n n ℂ}
66     (hp : rho.PosSemidef) (ht : Matrix.trace rho = 1) :
67     (channel K rho).PosSemidef ∧ Matrix.trace (channel K rho) = 1 := by
68   exact ⟨channel_positive K hp, (channel_trace_preserving K hK rho).trans ht⟩
69 end KomorebiPaperVII.Kraus
70 
71 #print axioms KomorebiPaperVII.Kraus.channel_add
72 #print axioms KomorebiPaperVII.Kraus.channel_smul
73 #print axioms KomorebiPaperVII.Kraus.channel_positive
74 #print axioms KomorebiPaperVII.Kraus.channel_trace_preserving
75 #print axioms KomorebiPaperVII.Kraus.amplification_eq_kraus
76 #print axioms KomorebiPaperVII.Kraus.channel_completely_positive
77 #print axioms KomorebiPaperVII.Kraus.channel_density_matrix

Back to source controls