LeakageBound.lean

1 module
2 public import Mathlib.Analysis.CStarAlgebra.Classes
3 public import Mathlib.Analysis.CStarAlgebra.Basic
4 public import Mathlib.Analysis.SpecialFunctions.Exponential
5 public import Mathlib.Analysis.Calculus.MeanValue
6 public import Mathlib.Analysis.CStarAlgebra.Matrix
7 public import Mathlib.LinearAlgebra.Matrix.Hermitian
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Paper VII, fourth block.
10 Quantitative leakage for the actual exponential, proved from its derivative.
11 The norm is the C-star norm, specialized below to the matrix operator norm. -/
12 public section
13 set_option autoImplicit false
14 set_option linter.unusedSectionVars false
15 namespace KomorebiPaperVII.Leakage
16 open NormedSpace
17 open scoped Matrix.Norms.L2Operator
18 variable {A : Type*} [CStarAlgebra A]
19 noncomputable local instance : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
20 
21 /-- Conjugation by the actual exponential of a fixed generator. -/
22 noncomputable def transported (G P : A) (t : ℝ) : A :=
23   exp (t • G) * P * exp (t • (-G))
24 
25 theorem exp_unitary (G : A) (hG : star G = -G) (t : ℝ) :
26     exp (t • G) ∈ unitary A := by
27   apply exp_mem_unitary_of_mem_skewAdjoint
28   change star (t • G) = -(t • G)
29   simp [hG]
30 
31 theorem transported_derivative (G P : A) (t : ℝ) :
32     HasDerivAt (transported G P)
33       (exp (t • G) * (G * P - P * G) * exp (t • (-G))) t := by
34   have hd := ((hasDerivAt_exp_smul_const G t).mul_const P).mul
35     (hasDerivAt_exp_smul_const' (-G) t)
36   convert hd using 1
37   · rfl
38   · noncomm_ring
39 
40 theorem transported_derivative_norm (G P : A) (hG : star G = -G) (t : ℝ) :
41     ‖deriv (transported G P) t‖ = ‖G * P - P * G‖ := by
42   rw [(transported_derivative G P t).deriv,
43     CStarRing.norm_mul_mem_unitary _ (exp_unitary (-G) (by simp [hG]) t),
44     CStarRing.norm_mem_unitary_mul _ (exp_unitary G hG t)]
45 
46 theorem transported_lipschitz (G P : A) (hG : star G = -G) (t s : ℝ) :
47     ‖transported G P t - transported G P s‖ ≤
48       |t-s| * ‖G*P-P*G‖ := by
49   have hh := Convex.norm_image_sub_le_of_norm_deriv_le
50     (f := transported G P) (s := Set.univ)
51     (fun x _ => (transported_derivative G P x).differentiableAt)
52     (fun x _ => (transported_derivative_norm G P hG x).le)
53     convex_univ (Set.mem_univ s) (Set.mem_univ t)
54   simpa [Real.norm_eq_abs, mul_comm] using hh
55 
56 theorem exponential_commutator_bound (G P : A) (hG : star G = -G) (t : ℝ) :
57     ‖exp (t • G) * P - P * exp (t • G)‖ ≤ |t| * ‖G*P-P*G‖ := by
58   have hcancel : exp (t • (-G)) * exp (t • G) = 1 := by
59     rw [smul_neg, ← exp_add_of_commute ((Commute.refl (t • G)).neg_left),
60       neg_add_cancel, NormedSpace.exp_zero]
61   have heq : (transported G P t - P) * exp (t • G) =
62       exp (t • G) * P - P * exp (t • G) := by
63     simp only [transported, sub_mul, mul_assoc, hcancel, mul_one]
64   rw [← heq, CStarRing.norm_mul_mem_unitary _ (exp_unitary G hG t)]
65   simpa [transported] using transported_lipschitz G P hG t 0
66 
67 theorem leakage_corner (P U : A) (hP : IsStarProjection P) :
68     (1-P)*U*P = (1-P)*(U*P-P*U)*P := by
69   symm
70   rw [mul_sub, sub_mul]
71   have hzero : (1-P)*(P*U)*P = 0 := by
72     rw [← mul_assoc (1-P) P U, hP.one_sub_mul_self, zero_mul, zero_mul]
73   rw [hzero, sub_zero, mul_assoc (1-P), mul_assoc U, hP.isIdempotentElem.eq, mul_assoc]
74 
75 theorem leakage_corner_norm (P U : A) (hP : IsStarProjection P) :
76     ‖(1-P)*U*P‖ ≤ ‖U*P-P*U‖ := by
77   rw [leakage_corner P U hP]
78   calc
79     _ ≤ ‖(1-P)*(U*P-P*U)‖ * ‖P‖ := norm_mul_le _ _
80     _ ≤ (‖1-P‖ * ‖U*P-P*U‖) * ‖P‖ :=
81       mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _)
82     _ ≤ (1 * ‖U*P-P*U‖) * 1 := by
83       gcongr
84       · exact IsStarProjection.norm_le _ hP.one_sub
85       · exact IsStarProjection.norm_le _ hP
86     _ = _ := by ring
87 
88 theorem skew_generator_leakage_bound (G P : A) (hG : star G = -G)
89     (hP : IsStarProjection P) (t : ℝ) :
90     ‖(1-P) * exp (t • G) * P‖ ≤ |t| * ‖G*P-P*G‖ :=
91   (leakage_corner_norm P _ hP).trans (exponential_commutator_bound G P hG t)
92 
93 /-- Schrodinger generator with the sign fixed by exp(-itH). -/
94 noncomputable def generator (H : A) : A := (-Complex.I) • H
95 
96 theorem generator_skew (H : A) (hH : IsSelfAdjoint H) :
97     star (generator H) = -generator H := by
98   simp [generator, star_smul, hH.star_eq]
99 
100 theorem generator_commutator_norm (H P : A) :
101     ‖generator H * P - P * generator H‖ = ‖H*P-P*H‖ := by
102   simp only [generator, smul_mul_assoc, mul_smul_comm, ← smul_sub, norm_smul,
103     norm_neg, Complex.norm_I, one_mul]
104 
105 /-- Theorem 5.2 with no nonzero-rank or nonzero-time restriction. -/
106 theorem commutator_leakage_bound (H P : A) (hH : IsSelfAdjoint H)
107     (hP : IsStarProjection P) (t : ℝ) :
108     ‖(1-P) * exp ((-(t : ℂ)*Complex.I) • H) * P‖ ≤ |t| * ‖H*P-P*H‖ := by
109   have hh := skew_generator_leakage_bound (generator H) P (generator_skew H hH) hP t
110   rw [generator_commutator_norm] at hh
111   convert hh using 1
112   simp [generator, ← Complex.real_smul]
113 
114 theorem exact_symmetry_zero_leakage (H P : A) (hH : IsSelfAdjoint H)
115     (hP : IsStarProjection P) (hcomm : H*P=P*H) (t : ℝ) :
116     (1-P) * exp ((-(t : ℂ)*Complex.I) • H) * P = 0 := by
117   apply norm_eq_zero.mp
118   apply le_antisymm _ (norm_nonneg _)
119   simpa [hcomm] using commutator_leakage_bound H P hH hP t
120 
121 /-- Leakage never exceeds one in the C-star norm, including zero projectors. -/
122 theorem unitary_corner_norm (P U : A) (hP : IsStarProjection P)
123     (hU : U ∈ unitary A) : ‖(1-P)*U*P‖ ≤ 1 := by
124   calc
125     _ ≤ ‖(1-P)*U‖*‖P‖ := norm_mul_le _ _
126     _ = ‖1-P‖*‖P‖ := by rw [CStarRing.norm_mul_mem_unitary _ hU]
127     _ ≤ 1*1 := by
128       gcongr
129       · exact IsStarProjection.norm_le _ hP.one_sub
130       · exact IsStarProjection.norm_le _ hP
131     _ = 1 := by norm_num
132 
133 theorem capped_commutator_leakage_bound (H P : A) (hH : IsSelfAdjoint H)
134     (hP : IsStarProjection P) (t : ℝ) :
135     ‖(1-P)*exp ((-(t : ℂ)*Complex.I) • H)*P‖ ≤ min 1 (|t| *‖H*P-P*H‖) := by
136   have hu : exp ((-(t : ℂ)*Complex.I) • H) ∈ unitary A := by
137     convert exp_unitary (generator H) (generator_skew H hH) t using 1
138     simp [generator, ← Complex.real_smul]
139   exact le_min (unitary_corner_norm P _ hP hu) (commutator_leakage_bound H P hH hP t)
140 
141 theorem projection_commutator_norm_le (V P : A) (hP : IsStarProjection P) :
142     ‖V*P-P*V‖ ≤ 2*‖V‖ := by
143   calc
144     _ ≤ ‖V*P‖+‖P*V‖ := norm_sub_le _ _
145     _ ≤ ‖V‖*‖P‖+‖P‖*‖V‖ := add_le_add (norm_mul_le _ _) (norm_mul_le _ _)
146     _ ≤ ‖V‖*1+1*‖V‖ := by
147       gcongr <;> exact IsStarProjection.norm_le _ hP
148     _ = 2*‖V‖ := by ring
149 
150 /-- A certified perturbation estimate when only the perturbation breaks symmetry. -/
151 theorem perturbation_leakage_bound (H₀ V P : A)
152     (hH₀ : IsSelfAdjoint H₀) (hV : IsSelfAdjoint V)
153     (hP : IsStarProjection P) (hcomm : H₀*P=P*H₀) (t : ℝ) :
154     ‖(1-P)*exp ((-(t : ℂ)*Complex.I) • (H₀+V))*P‖ ≤ 2*|t| *‖V‖ := by
155   have hc : (H₀+V)*P-P*(H₀+V) = V*P-P*V := by
156     rw [add_mul, mul_add, hcomm]
157     noncomm_ring
158   have hh := commutator_leakage_bound (H₀+V) P (hH₀.add hV) hP t
159   rw [hc] at hh
160   calc
161     _ ≤ |t| *‖V*P-P*V‖ := hh
162     _ ≤ |t| *(2*‖V‖) := mul_le_mul_of_nonneg_left
163       (projection_commutator_norm_le V P hP) (abs_nonneg t)
164     _ = _ := by ring
165 
166 /-- Concrete complex matrices, equipped with the operator norm. -/
167 theorem matrix_commutator_leakage_bound {n : Type*} [Fintype n] [DecidableEq n]
168     (H P : Matrix n n ℂ) (hH : H.IsHermitian) (hP : P.IsHermitian)
169     (hPP : P*P=P) (t : ℝ) :
170     ‖(1-P) * exp ((-(t : ℂ)*Complex.I) • H) * P‖ ≤ |t| * ‖H*P-P*H‖ := by
171   exact commutator_leakage_bound H P hH.isSelfAdjoint ⟨hPP, hP.isSelfAdjoint⟩ t
172 end KomorebiPaperVII.Leakage
173 
174 /-! Complete declaration-level trust audit. -/
175 #print axioms KomorebiPaperVII.Leakage.exp_unitary
176 #print axioms KomorebiPaperVII.Leakage.transported_derivative
177 #print axioms KomorebiPaperVII.Leakage.transported_derivative_norm
178 #print axioms KomorebiPaperVII.Leakage.transported_lipschitz
179 #print axioms KomorebiPaperVII.Leakage.exponential_commutator_bound
180 #print axioms KomorebiPaperVII.Leakage.leakage_corner
181 #print axioms KomorebiPaperVII.Leakage.leakage_corner_norm
182 #print axioms KomorebiPaperVII.Leakage.skew_generator_leakage_bound
183 #print axioms KomorebiPaperVII.Leakage.generator_skew
184 #print axioms KomorebiPaperVII.Leakage.generator_commutator_norm
185 #print axioms KomorebiPaperVII.Leakage.commutator_leakage_bound
186 #print axioms KomorebiPaperVII.Leakage.exact_symmetry_zero_leakage
187 #print axioms KomorebiPaperVII.Leakage.unitary_corner_norm
188 #print axioms KomorebiPaperVII.Leakage.capped_commutator_leakage_bound
189 #print axioms KomorebiPaperVII.Leakage.projection_commutator_norm_le
190 #print axioms KomorebiPaperVII.Leakage.perturbation_leakage_bound
191 #print axioms KomorebiPaperVII.Leakage.matrix_commutator_leakage_bound

Back to source controls