SyndromeRecovery.lean

1 module
2 public import Mathlib.Algebra.Star.StarProjection
3 public import Mathlib.Algebra.Star.BigOperators
4 public import Mathlib.LinearAlgebra.Matrix.PosDef
5 public import Mathlib.LinearAlgebra.Matrix.Trace
6 public import Mathlib.LinearAlgebra.Matrix.Kronecker
7 public import Mathlib.Analysis.Complex.Basic
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Paper VII, fourth block.
10 Constructive recovery from an orthogonal partial-isometry syndrome family.
11 This is the recovery stage of Knill-Laflamme, not its full necessity or the
12 spectral reduction from an arbitrary positive Gram matrix. -/
13 public section
14 set_option autoImplicit false
15 set_option backward.isDefEq.respectTransparency false
16 set_option backward.isDefEq.respectTransparency.types false
17 set_option linter.unusedSectionVars false
18 namespace KomorebiPaperVII.Recovery
19 open scoped BigOperators Kronecker ComplexOrder
20 
21 structure OrthogonalSyndromes (R I : Type*) [Ring R] [StarRing R]
22     [Fintype I] [DecidableEq I] where
23   code : R
24   code_projection : IsStarProjection code
25   error : I → R
26   restricted : ∀ a, error a * code = error a
27   gram : ∀ a b, star (error a) * error b = if a=b then code else 0
28 
29 namespace OrthogonalSyndromes
30 variable {R I : Type*} [Ring R] [StarRing R] [Fintype I] [DecidableEq I]
31 variable (S : OrthogonalSyndromes R I)
32 
33 def packet (a : I) : R := S.error a * star (S.error a)
34 def total : R := ∑ a, S.packet a
35 def complement : R := 1-S.total
36 
37 theorem packet_selfAdjoint (a : I) : IsSelfAdjoint (S.packet a) := by
38   change star (S.packet a) = S.packet a
39   simp [packet]
40 
41 theorem packet_mul (a b : I) : S.packet a * S.packet b =
42     if a=b then S.packet a else 0 := by
43   have heq : S.packet a * S.packet b =
44       S.error a * (star (S.error a) * S.error b) * star (S.error b) := by
45     unfold packet
46     noncomm_ring
47   rw [heq, S.gram]
48   by_cases h : a=b
49   · subst b
50     simp [S.restricted, packet]
51   · simp [h]
52 
53 theorem total_projection : IsStarProjection S.total := by
54   constructor
55   · change S.total*S.total=S.total
56     simp [total, Finset.sum_mul, Finset.mul_sum, S.packet_mul]
57   · change star (∑ a, S.packet a) = ∑ a, S.packet a
58     rw [star_sum]
59     exact Finset.sum_congr rfl (fun a _ => (S.packet_selfAdjoint a).star_eq)
60 
61 theorem complement_projection : IsStarProjection S.complement :=
62   S.total_projection.one_sub
63 
64 theorem total_error (a : I) : S.total*S.error a = S.error a := by
65   simp only [total, Finset.sum_mul, packet, mul_assoc, S.gram]
66   simp [mul_ite, S.restricted]
67 
68 theorem complement_error (a : I) : S.complement*S.error a = 0 := by
69   simp [complement, sub_mul, S.total_error]
70 
71 theorem error_adjoint_complement (a : I) : star (S.error a)*S.complement = 0 := by
72   have hh := congrArg star (S.complement_error a)
73   simpa [star_mul, S.complement_projection.isSelfAdjoint.star_eq] using hh
74 
75 /-- A total, trace-preserving extension: the unused complement is retained. -/
76 def decoder (rho : R) : R :=
77   (∑ a, star (S.error a)*rho*S.error a) + S.complement*rho*S.complement
78 
79 /-- Includes the complement Kraus operator rather than silently discarding it. -/
80 def recoveryKraus : Option I → R
81   | none => S.complement
82   | some a => star (S.error a)
83 
84 theorem recoveryKraus_complete :
85     (∑ a, star (S.recoveryKraus a)*S.recoveryKraus a) = 1 := by
86   rw [Fintype.sum_option]
87   simp only [recoveryKraus, star_star, S.complement_projection.isSelfAdjoint.star_eq,
88     S.complement_projection.isIdempotentElem.eq]
89   change S.complement + S.total = 1
90   simp [complement]
91 
92 theorem decoder_eq_kraus (rho : R) :
93     S.decoder rho = ∑ a, S.recoveryKraus a*rho*star (S.recoveryKraus a) := by
94   rw [Fintype.sum_option]
95   simp [decoder, recoveryKraus, S.complement_projection.isSelfAdjoint.star_eq, add_comm]
96 
97 theorem decoder_add (rho sigma : R) :
98     S.decoder (rho+sigma) = S.decoder rho + S.decoder sigma := by
99   simp only [decoder, mul_add, add_mul, Finset.sum_add_distrib]
100   abel
101 
102 /-- Every off-diagonal syndrome term is removed, every diagonal one decoded. -/
103 theorem decoder_cross_error (rho : R) (hrho : S.code*rho*S.code=rho) (a b : I) :
104     S.decoder (S.error a*rho*star (S.error b)) = if a=b then rho else 0 := by
105   have hc (c : I) :
106       star (S.error c)*(S.error a*rho*star (S.error b))*S.error c =
107         if c=a then (if a=b then rho else 0) else 0 := by
108     have heq : star (S.error c)*(S.error a*rho*star (S.error b))*S.error c =
109         (star (S.error c)*S.error a)*rho*(star (S.error b)*S.error c) := by
110       noncomm_ring
111     rw [heq, S.gram, S.gram]
112     by_cases hca : c=a
113     · subst c
114       by_cases hab : a=b
115       · subst b; simp [hrho]
116       · simp [hab, Ne.symm hab]
117     · simp [hca]
118   have hq : S.complement*(S.error a*rho*star (S.error b))*S.complement=0 := by
119     calc
120       _ = (S.complement*S.error a)*rho*(star (S.error b)*S.complement) := by
121         noncomm_ring
122       _ = 0 := by rw [S.complement_error, zero_mul, zero_mul]
123   simp only [decoder, hc, hq, add_zero]
124   simp
125 
126 section Scalars
127 variable [Algebra ℂ R] [StarModule ℂ R]
128 
129 theorem decoder_smul (z : ℂ) (rho : R) : S.decoder (z • rho) = z • S.decoder rho := by
130   simp [decoder, Finset.smul_sum, smul_add]
131 
132 def decoderLinear : R →ₗ[ℂ] R where
133   toFun := S.decoder
134   map_add' := S.decoder_add
135   map_smul' := S.decoder_smul
136 
137 /-- Exact recovery of every normalized mixture of the certified syndrome errors. -/
138 theorem decoder_weighted_noise (rho : R) (hrho : S.code*rho*S.code=rho)
139     (weights : I → ℂ) (hweights : ∑ a, weights a=1) :
140     S.decoder (∑ a, weights a • (S.error a*rho*star (S.error a))) = rho := by
141   change S.decoderLinear (∑ a, weights a • (S.error a*rho*star (S.error a))) = rho
142   rw [map_sum]
143   simp only [map_smul]
144   change (∑ a, weights a • S.decoder (S.error a*rho*star (S.error a))) = rho
145   simp_rw [S.decoder_cross_error rho hrho, ite_true]
146   rw [← Finset.sum_smul, hweights, one_smul]
147 
148 /-- Coherent error superpositions are corrected with their exact norm factor. -/
149 theorem decoder_error_superposition (rho : R) (hrho : S.code*rho*S.code=rho)
150     (z : I → ℂ) :
151     S.decoder ((∑ a, z a • S.error a)*rho*star (∑ b, z b • S.error b)) =
152       (∑ a, z a * star (z a)) • rho := by
153   have heq : (∑ a, z a • S.error a)*rho*star (∑ b, z b • S.error b) =
154       ∑ a, ∑ b, (z a * star (z b)) • (S.error a*rho*star (S.error b)) := by
155     rw [star_sum]
156     simp only [star_smul]
157     rw [Finset.sum_mul, Finset.sum_mul]
158     simp only [Finset.mul_sum]
159     apply Finset.sum_congr rfl
160     intro a _
161     apply Finset.sum_congr rfl
162     intro b _
163     simp only [smul_mul_assoc, mul_smul_comm, smul_smul]
164     rw [mul_comm]
165   rw [heq]
166   change S.decoderLinear (∑ a, ∑ b, (z a * star (z b)) •
167     (S.error a*rho*star (S.error b))) = _
168   simp only [map_sum, map_smul]
169   change (∑ a, ∑ b, (z a * star (z b)) • S.decoder
170     (S.error a*rho*star (S.error b))) = _
171   simp_rw [S.decoder_cross_error rho hrho]
172   simp [smul_ite, Finset.sum_smul]
173 end Scalars
174 end OrthogonalSyndromes
175 
176 section Matrices
177 variable {n I : Type*} [Fintype n] [DecidableEq n] [Fintype I] [DecidableEq I]
178 variable (S : OrthogonalSyndromes (Matrix n n ℂ) I)
179 
180 theorem recovery_positive {rho : Matrix n n ℂ} (hrho : rho.PosSemidef) :
181     (S.decoder rho).PosSemidef := by
182   rw [S.decoder_eq_kraus]
183   exact Matrix.posSemidef_sum _ (fun a _ =>
184     hrho.mul_mul_conjTranspose_same (S.recoveryKraus a))
185 
186 theorem recovery_trace_preserving (rho : Matrix n n ℂ) :
187     Matrix.trace (S.decoder rho) = Matrix.trace rho := by
188   rw [S.decoder_eq_kraus, Matrix.trace_sum]
189   have cyclic (a : Option I) :
190       Matrix.trace (S.recoveryKraus a*rho*star (S.recoveryKraus a)) =
191         Matrix.trace ((star (S.recoveryKraus a)*S.recoveryKraus a)*rho) := by
192     rw [Matrix.trace_mul_comm, Matrix.mul_assoc]
193   simp_rw [cyclic]
194   rw [← Matrix.trace_sum, ← Finset.sum_mul, S.recoveryKraus_complete, Matrix.one_mul]
195 
196 /-- The actual identity-tensor recovery, checked at every finite auxiliary dimension. -/
197 theorem recovery_complete_positivity {J : Type*} [Fintype J] [DecidableEq J]
198     {rho : Matrix (J × n) (J × n) ℂ} (hrho : rho.PosSemidef) :
199     Matrix.PosSemidef (fun (x y : J × n) =>
200       S.decoder (fun u v => rho (x.1,u) (y.1,v)) x.2 y.2) := by
201   have heq : (fun (x y : J × n) => S.decoder (fun u v => rho (x.1,u) (y.1,v)) x.2 y.2) =
202       ∑ a, ((1 : Matrix J J ℂ) ⊗ₖ S.recoveryKraus a)*rho*
203         (((1 : Matrix J J ℂ) ⊗ₖ S.recoveryKraus a).conjTranspose) := by
204     ext ⟨i,u⟩ ⟨j,v⟩
205     simp_rw [S.decoder_eq_kraus, Matrix.sum_apply, Matrix.mul_apply,
206       Matrix.conjTranspose_apply, Matrix.kroneckerMap_apply]
207     simp [Fintype.sum_prod_type, Matrix.one_apply, apply_ite]
208   rw [heq]
209   exact Matrix.posSemidef_sum _ (fun a _ =>
210     hrho.mul_mul_conjTranspose_same ((1 : Matrix J J ℂ) ⊗ₖ S.recoveryKraus a))
211 
212 theorem recovery_density_matrix {rho : Matrix n n ℂ}
213     (hrho : rho.PosSemidef) (htrace : Matrix.trace rho=1) :
214     (S.decoder rho).PosSemidef ∧ Matrix.trace (S.decoder rho)=1 :=
215   ⟨recovery_positive S hrho, (recovery_trace_preserving S rho).trans htrace⟩
216 end Matrices
217 end KomorebiPaperVII.Recovery
218 
219 /-! Complete declaration-level trust audit. -/
220 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.packet_selfAdjoint
221 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.packet_mul
222 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.total_projection
223 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.complement_projection
224 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.total_error
225 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.complement_error
226 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.error_adjoint_complement
227 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.recoveryKraus_complete
228 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_eq_kraus
229 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_add
230 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_cross_error
231 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_smul
232 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_weighted_noise
233 #print axioms KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder_error_superposition
234 #print axioms KomorebiPaperVII.Recovery.recovery_positive
235 #print axioms KomorebiPaperVII.Recovery.recovery_trace_preserving
236 #print axioms KomorebiPaperVII.Recovery.recovery_complete_positivity
237 #print axioms KomorebiPaperVII.Recovery.recovery_density_matrix

Back to source controls