KnillLaflammeSufficiency.lean

1 module
2 public import SyndromeRecovery
3 import all SyndromeRecovery
4 public import Mathlib.Analysis.Matrix.PosDef
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Paper VII fifth block.
7 Spectral reduction of general Knill-Laflamme data, retaining singular Gram matrices.
8 -/
9 public section
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 set_option backward.isDefEq.respectTransparency.types false
13 set_option linter.unusedSectionVars false
14 namespace KomorebiPaperVII.KnillLaflamme
15 open scoped BigOperators ComplexOrder
16 open Matrix
17 open KomorebiPaperVII.Recovery
18 variable {n I : Type*} [Fintype n] [DecidableEq n] [Fintype I] [DecidableEq I]
19 
20 /-- A change of coordinates in the error index, with columns as new errors. -/
21 def mix (E : I → Matrix n n ℂ) (U : Matrix I I ℂ) (r : I) : Matrix n n ℂ :=
22   ∑ a, U a r • E a
23 
24 /-- Unnormalized finite Kraus sum. -/
25 def noise (E : I → Matrix n n ℂ) (rho : Matrix n n ℂ) : Matrix n n ℂ :=
26   ∑ a, E a * rho * star (E a)
27 
28 theorem mix_restricted (P : Matrix n n ℂ) (E : I → Matrix n n ℂ)
29     (hE : ∀ a, E a * P = E a) (U : Matrix I I ℂ) (r : I) :
30     mix E U r * P = mix E U r := by
31   simp [mix, Finset.sum_mul, hE]
32 
33 theorem mix_gram (P : Matrix n n ℂ) (E : I → Matrix n n ℂ)
34     (C : Matrix I I ℂ) (hC : ∀ a b, star (E a) * E b = C a b • P)
35     (U : Matrix I I ℂ) (r s : I) :
36     star (mix E U r) * mix E U s = (star U * C * U) r s • P := by
37   simp only [mix, star_sum, star_smul, Finset.sum_mul, Finset.mul_sum,
38     smul_mul_assoc, mul_smul_comm, smul_smul, hC]
39   simp only [smul_smul, Matrix.mul_apply, Matrix.star_apply, ← Finset.sum_smul]
40   congr 1
41   apply Finset.sum_congr rfl
42   intro b _
43   ring
44 
45 theorem mix_noise (E : I → Matrix n n ℂ) (U : Matrix.unitaryGroup I ℂ)
46     (rho : Matrix n n ℂ) : noise (mix E (U : Matrix I I ℂ)) rho = noise E rho := by
47   have hU (a b : I) : (∑ r, (U : Matrix I I ℂ) a r * star ((U : Matrix I I ℂ) b r)) =
48       if a=b then 1 else 0 := by
49     simpa [Matrix.mul_apply, Matrix.star_apply, Matrix.one_apply] using
50       congrArg (fun M : Matrix I I ℂ => M a b) (Unitary.coe_mul_star_self U)
51   have heq (r : I) : mix E (U : Matrix I I ℂ) r * rho * star (mix E (U : Matrix I I ℂ) r) =
52       ∑ a, ∑ b, ((U : Matrix I I ℂ) a r * star ((U : Matrix I I ℂ) b r)) •
53         (E a * rho * star (E b)) := by
54     unfold mix
55     rw [star_sum]
56     simp only [star_smul]
57     rw [Finset.sum_mul, Finset.sum_mul]
58     simp only [Finset.mul_sum]
59     apply Finset.sum_congr rfl
60     intro a _
61     apply Finset.sum_congr rfl
62     intro b _
63     simp only [smul_mul_assoc, mul_smul_comm, smul_smul]
64     rw [mul_comm]
65   unfold noise
66   simp_rw [heq]
67   rw [Finset.sum_comm]
68   apply Finset.sum_congr rfl
69   intro a _
70   rw [Finset.sum_comm]
71   simp_rw [← Finset.sum_smul, hU]
72   simp
73 
74 theorem diagonalized_gram (P : Matrix n n ℂ) (E : I → Matrix n n ℂ)
75     (C : Matrix I I ℂ) (hC : C.PosSemidef)
76     (hgram : ∀ a b, star (E a) * E b = C a b • P) (r s : I) :
77     star (mix E (hC.isHermitian.eigenvectorUnitary : Matrix I I ℂ) r) *
78       mix E (hC.isHermitian.eigenvectorUnitary : Matrix I I ℂ) s =
79         if r=s then (hC.isHermitian.eigenvalues r : ℂ) • P else 0 := by
80   rw [mix_gram P E C hgram]
81   have hdiag : star (hC.isHermitian.eigenvectorUnitary : Matrix I I ℂ) * C *
82       (hC.isHermitian.eigenvectorUnitary : Matrix I I ℂ) =
83         diagonal (fun r => (hC.isHermitian.eigenvalues r : ℂ)) := by
84     simpa [Unitary.conjStarAlgAut_star_apply, Function.comp_def] using
85       hC.isHermitian.conjStarAlgAut_star_eigenvectorUnitary
86   rw [hdiag]
87   by_cases h : r=s
88   · subst s; simp
89   · simp [h]
90 
91 
92 /-- Diagonal Gram data. Weights may vanish; no invertibility is assumed. -/
93 structure DiagonalErrors (n I : Type*) [Fintype n] [DecidableEq n]
94     [Fintype I] [DecidableEq I] where
95   code : Matrix n n ℂ
96   code_projection : IsStarProjection code
97   error : I → Matrix n n ℂ
98   restricted : ∀ a, error a * code = error a
99   weight : I → ℝ
100   nonnegative : ∀ a, 0 ≤ weight a
101   gram : ∀ a b, star (error a) * error b = if a=b then (weight a : ℂ) • code else 0
102 
103 namespace DiagonalErrors
104 variable (D : DiagonalErrors n I)
105 
106 /-- Null eigenvalue directions vanish on the code. -/
107 theorem zero_weight_error (a : I) (ha : D.weight a = 0) : D.error a = 0 := by
108   have hh : star (D.error a) * D.error a = 0 := by
109     simpa only [ite_true, ha, Complex.ofReal_zero, zero_smul] using D.gram a a
110   exact Matrix.conjTranspose_mul_self_eq_zero.mp hh
111 
112 /-- Only strictly positive eigenvalues are normalized. -/
113 abbrev Active := {a : I // 0 < D.weight a}
114 
115 noncomputable def normalizedError (a : D.Active) : Matrix n n ℂ :=
116   (Real.sqrt (D.weight a) : ℂ)⁻¹ • D.error a
117 
118 theorem sqrt_weight_ne_zero (a : D.Active) : (Real.sqrt (D.weight a) : ℂ) ≠ 0 := by
119   exact_mod_cast (ne_of_gt (Real.sqrt_pos.mpr a.property))
120 
121 theorem sqrt_weight_sq (a : I) :
122     (Real.sqrt (D.weight a) : ℂ) * (Real.sqrt (D.weight a) : ℂ) = (D.weight a : ℂ) := by
123   exact_mod_cast Real.mul_self_sqrt (D.nonnegative a)
124 
125 theorem normalized_restricted (a : D.Active) : D.normalizedError a * D.code = D.normalizedError a := by
126   simp [normalizedError, D.restricted]
127 
128 theorem normalized_gram (a b : D.Active) :
129     star (D.normalizedError a) * D.normalizedError b = if a=b then D.code else 0 := by
130   simp only [normalizedError, star_smul, smul_mul_assoc, mul_smul_comm, smul_smul, D.gram]
131   by_cases h : a=b
132   · subst b
133     simp only [ite_true, smul_smul]
134     have hs : star ((Real.sqrt (D.weight a) : ℂ)⁻¹) = (Real.sqrt (D.weight a) : ℂ)⁻¹ := by simp
135     rw [hs]
136     have heq : (Real.sqrt (D.weight a) : ℂ)⁻¹ *
137         (Real.sqrt (D.weight a) : ℂ)⁻¹ * (D.weight a : ℂ) = 1 := by
138       rw [← D.sqrt_weight_sq]
139       field_simp [D.sqrt_weight_ne_zero a]
140     rw [heq, one_smul]
141   · have hab : (a : I) ≠ (b : I) := fun h' => h (Subtype.ext h')
142     simp [h, hab]
143 
144 /-- The previous block's recovery object, now constructed from diagonal Gram data. -/
145 noncomputable def syndromes : OrthogonalSyndromes (Matrix n n ℂ) D.Active where
146   code := D.code
147   code_projection := D.code_projection
148   error := D.normalizedError
149   restricted := D.normalized_restricted
150   gram := D.normalized_gram
151 
152 theorem error_eq_sqrt_normalized (a : D.Active) :
153     D.error a = (Real.sqrt (D.weight a) : ℂ) • D.normalizedError a := by
154   simp [normalizedError, smul_smul, D.sqrt_weight_ne_zero a]
155 
156 theorem decode_diagonal_error (rho : Matrix n n ℂ) (hrho : D.code*rho*D.code=rho) (a : I) :
157     D.syndromes.decoder (D.error a*rho*star (D.error a)) = (D.weight a : ℂ) • rho := by
158   by_cases ha : 0 < D.weight a
159   · let a' : D.Active := ⟨a,ha⟩
160     have heq := D.error_eq_sqrt_normalized a'
161     change D.error a = _ at heq
162     rw [heq]
163     simp only [star_smul, smul_mul_assoc, mul_smul_comm, smul_smul,
164       Complex.star_def, Complex.conj_ofReal]
165     rw [D.syndromes.decoder_smul]
166     change ((Real.sqrt (D.weight a) : ℂ) * (Real.sqrt (D.weight a) : ℂ)) •
167       D.syndromes.decoder (D.syndromes.error a'*rho*star (D.syndromes.error a')) = _
168     rw [D.syndromes.decoder_cross_error rho hrho]
169     simp [D.sqrt_weight_sq]
170   · have hz : D.weight a = 0 := le_antisymm (le_of_not_gt ha) (D.nonnegative a)
171     rw [D.zero_weight_error a hz]
172     simp only [zero_mul, star_zero, mul_zero, hz, Complex.ofReal_zero, zero_smul]
173     exact D.syndromes.decoderLinear.map_zero
174 
175 theorem decode_noise (rho : Matrix n n ℂ) (hrho : D.code*rho*D.code=rho) :
176     D.syndromes.decoder (noise D.error rho) = (∑ a, (D.weight a : ℂ)) • rho := by
177   change D.syndromes.decoderLinear (∑ a, D.error a*rho*star (D.error a)) = _
178   rw [map_sum]
179   change (∑ a, D.syndromes.decoder (D.error a*rho*star (D.error a))) = _
180   simp_rw [D.decode_diagonal_error rho hrho]
181   rw [Finset.sum_smul]
182 
183 end DiagonalErrors
184 
185 
186 /-- General finite Knill-Laflamme Gram data, not pre-diagonalized syndrome data. -/
187 structure Data (n I : Type*) [Fintype n] [DecidableEq n] [Fintype I] [DecidableEq I] where
188   code : Matrix n n ℂ
189   code_projection : IsStarProjection code
190   error : I → Matrix n n ℂ
191   gramMatrix : Matrix I I ℂ
192   gram_positive : gramMatrix.PosSemidef
193   gram : ∀ a b, code * star (error a) * error b * code = gramMatrix a b • code
194 
195 namespace Data
196 variable (K : Data n I)
197 
198 theorem restricted_error_gram (a b : I) :
199     star (K.error a*K.code) * (K.error b*K.code) = K.gramMatrix a b • K.code := by
200   rw [star_mul, K.code_projection.isSelfAdjoint.star_eq]
201   simpa only [mul_assoc] using K.gram a b
202 
203 /-- Actual spectral construction from the positive Gram matrix. -/
204 noncomputable def diagonal : DiagonalErrors n I where
205   code := K.code
206   code_projection := K.code_projection
207   error := mix (fun a => K.error a*K.code)
208     (K.gram_positive.isHermitian.eigenvectorUnitary : Matrix I I ℂ)
209   restricted := mix_restricted K.code (fun a => K.error a*K.code)
210     (fun a => by rw [mul_assoc, K.code_projection.isIdempotentElem.eq]) _
211   weight := K.gram_positive.isHermitian.eigenvalues
212   nonnegative := K.gram_positive.eigenvalues_nonneg
213   gram := diagonalized_gram K.code (fun a => K.error a*K.code) K.gramMatrix
214     K.gram_positive K.restricted_error_gram
215 
216 theorem restricted_noise (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) :
217     noise (fun a => K.error a*K.code) rho = noise K.error rho := by
218   unfold noise
219   apply Finset.sum_congr rfl
220   intro a _
221   rw [star_mul, K.code_projection.isSelfAdjoint.star_eq]
222   calc
223     (K.error a*K.code)*rho*(K.code*star (K.error a)) =
224       K.error a*(K.code*rho*K.code)*star (K.error a) := by noncomm_ring
225     _ = K.error a*rho*star (K.error a) := by rw [hrho]
226 
227 theorem diagonal_noise (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) :
228     noise K.diagonal.error rho = noise K.error rho := by
229   rw [diagonal, mix_noise, K.restricted_noise rho hrho]
230 
231 /-- The constructed recovery has the exact scale of the input error sum. -/
232 theorem recovery_noise_scaled (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) :
233     K.diagonal.syndromes.decoder (noise K.error rho) = Matrix.trace K.gramMatrix • rho := by
234   rw [← K.diagonal_noise rho hrho, K.diagonal.decode_noise rho hrho]
235   rw [K.gram_positive.isHermitian.trace_eq_sum_eigenvalues]
236   rfl
237 
238 theorem gram_trace_one (hcode : K.code ≠ 0)
239     (hcomplete : (∑ a, star (K.error a)*K.error a) = 1) : Matrix.trace K.gramMatrix = 1 := by
240   apply smul_left_injective ℂ hcode
241   change K.gramMatrix.trace • K.code = (1 : ℂ) • K.code
242   rw [one_smul, Matrix.trace, Finset.sum_smul]
243   change (∑ a, K.gramMatrix a a • K.code) = K.code
244   simp_rw [← K.gram]
245   calc
246     (∑ a, K.code*star (K.error a)*K.error a*K.code) =
247         K.code*(∑ a, star (K.error a)*K.error a)*K.code := by
248       simp only [Finset.sum_mul, Finset.mul_sum, mul_assoc]
249     _ = K.code := by rw [hcomplete, mul_one, K.code_projection.isIdempotentElem.eq]
250 
251 /-- Sufficiency for a normalized finite Kraus channel, including the zero code. -/
252 theorem recovery_corrects (hcomplete : (∑ a, star (K.error a)*K.error a) = 1)
253     (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) :
254     K.diagonal.syndromes.decoder (noise K.error rho) = rho := by
255   rw [K.recovery_noise_scaled rho hrho]
256   by_cases hp : K.code = 0
257   · have hr : rho=0 := by simpa [hp] using hrho.symm
258     simp [hr]
259   · rw [K.gram_trace_one hp hcomplete, one_smul]
260 
261 /-- The recovery is a channel on the entire ambient matrix space. -/
262 theorem recovery_complete :
263     (∑ a, star (K.diagonal.syndromes.recoveryKraus a)*
264       K.diagonal.syndromes.recoveryKraus a) = 1 :=
265   K.diagonal.syndromes.recoveryKraus_complete
266 
267 theorem recovery_preserves_trace (rho : Matrix n n ℂ) :
268     Matrix.trace (K.diagonal.syndromes.decoder rho) = Matrix.trace rho :=
269   recovery_trace_preserving K.diagonal.syndromes rho
270 
271 theorem recovery_completely_positive {J : Type*} [Fintype J] [DecidableEq J]
272     {rho : Matrix (J × n) (J × n) ℂ} (hrho : rho.PosSemidef) :
273     Matrix.PosSemidef (fun (x y : J × n) =>
274       K.diagonal.syndromes.decoder (fun u v => rho (x.1,u) (y.1,v)) x.2 y.2) :=
275   recovery_complete_positivity K.diagonal.syndromes hrho
276 
277 /-- A single existential certificate joining spectral reduction and the actual decoder. -/
278 theorem exists_recovery (hcomplete : (∑ a, star (K.error a)*K.error a) = 1) :
279     ∃ R : Option K.diagonal.Active → Matrix n n ℂ,
280       (∑ a, star (R a)*R a)=1 ∧
281       ∀ rho : Matrix n n ℂ, K.code*rho*K.code=rho →
282         (∑ a, R a*(noise K.error rho)*star (R a))=rho := by
283   refine ⟨K.diagonal.syndromes.recoveryKraus, K.recovery_complete, ?_⟩
284   intro rho hrho
285   rw [← K.diagonal.syndromes.decoder_eq_kraus]
286   exact K.recovery_corrects hcomplete rho hrho
287 
288 end Data
289 end KomorebiPaperVII.KnillLaflamme
290 
291 /-! Complete declaration-level trust audit. -/
292 #print axioms KomorebiPaperVII.KnillLaflamme.mix_restricted
293 #print axioms KomorebiPaperVII.KnillLaflamme.mix_gram
294 #print axioms KomorebiPaperVII.KnillLaflamme.mix_noise
295 #print axioms KomorebiPaperVII.KnillLaflamme.diagonalized_gram
296 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.zero_weight_error
297 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.sqrt_weight_ne_zero
298 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.sqrt_weight_sq
299 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.normalized_restricted
300 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.normalized_gram
301 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.error_eq_sqrt_normalized
302 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.decode_diagonal_error
303 #print axioms KomorebiPaperVII.KnillLaflamme.DiagonalErrors.decode_noise
304 #print axioms KomorebiPaperVII.KnillLaflamme.Data.restricted_error_gram
305 #print axioms KomorebiPaperVII.KnillLaflamme.Data.restricted_noise
306 #print axioms KomorebiPaperVII.KnillLaflamme.Data.diagonal_noise
307 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_noise_scaled
308 #print axioms KomorebiPaperVII.KnillLaflamme.Data.gram_trace_one
309 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_corrects
310 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_complete
311 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_preserves_trace
312 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_completely_positive
313 #print axioms KomorebiPaperVII.KnillLaflamme.Data.exists_recovery

Back to source controls