DiscoveryCertificate.lean

1 module
2 public import PacketIR
3 import all PacketIR
4 import all QuantumPacketCore
5 public import Mathlib.Analysis.Matrix.Normed
6 public import Mathlib.Analysis.CStarAlgebra.Matrix
7 public import Mathlib.LinearAlgebra.Matrix.Trace
8 public import Mathlib.Tactic
9 
10 /-!
11 Author: Komorebi P. Paper VIII item 9.2.
12 Exact residual of arbitrary complete orthogonal projector families, not only
13 coordinate masks. Frobenius and Euclidean operator norms are kept distinct.
14 This certifies a supplied decomposition; it does not discover the projectors.
15 -/
16 public section
17 set_option autoImplicit false
18 namespace KomorebiPaperVIII
19 open scoped BigOperators Classical Matrix
20 open KomorebiPaperVII
21 variable {X I : Type*} [Fintype X] [DecidableEq X] [Fintype I] [DecidableEq I]
22 variable (P : PacketFamily (Matrix X X ℂ) I)
23 
24 noncomputable def diagonalCompression (A : Matrix X X ℂ) : Matrix X X ℂ :=
25   ∑ a, P.block A a a
26 
27 noncomputable def offDiagonalTerm (A : Matrix X X ℂ) (e : I × I) : Matrix X X ℂ :=
28   if e.1 = e.2 then 0 else P.block A e.1 e.2
29 
30 theorem compression_decomposition (A : Matrix X X ℂ) :
31     A = diagonalCompression P A + ∑ e, offDiagonalTerm P A e := by
32   calc
33     A = ∑ b, ∑ a, ((if b=a then P.block A b a else 0) +
34         (if b=a then 0 else P.block A b a)) := by
35       conv_lhs => rw [←P.reconstruct A]
36       apply Finset.sum_congr rfl
37       intro b _
38       apply Finset.sum_congr rfl
39       intro a _
40       by_cases he : b=a <;> simp [he]
41     _ = diagonalCompression P A + ∑ e, offDiagonalTerm P A e := by
42       simp only [Finset.sum_add_distrib,Fintype.sum_prod_type,offDiagonalTerm,
43         diagonalCompression]
44       congr 1
45       apply Finset.sum_congr rfl
46       intro b _
47       simp
48 
49 theorem compression_residual (A : Matrix X X ℂ) :
50     A-diagonalCompression P A = ∑ e, offDiagonalTerm P A e := by
51   exact sub_eq_iff_eq_add.mpr ((compression_decomposition P A).trans (add_comm _ _))
52 
53 /-- Distinct packet corners are Hilbert--Schmidt orthogonal. -/
54 theorem block_trace_orthogonal (hP : ∀ a, (P.proj a)ᴴ = P.proj a)
55     (A B : Matrix X X ℂ) (b a d c : I) (hne : (b,a) ≠ (d,c)) :
56     Matrix.trace ((P.block A b a)ᴴ * P.block B d c) = 0 := by
57   have hadj : (P.block A b a)ᴴ = P.proj a*Aᴴ*P.proj b := by
58     simp only [PacketFamily.block,Matrix.conjTranspose_mul,hP,Matrix.mul_assoc]
59   rw [hadj]
60   by_cases hbd : b=d
61   · have hca : c ≠ a := by
62       intro he
63       apply hne
64       exact Prod.ext hbd he.symm
65     calc
66       Matrix.trace ((P.proj a*Aᴴ*P.proj b)*P.block B d c) =
67           Matrix.trace ((P.proj a*Aᴴ*P.proj b*P.proj d*B)*P.proj c) := by
68         simp only [PacketFamily.block,Matrix.mul_assoc]
69       _ = Matrix.trace (P.proj c*(P.proj a*Aᴴ*P.proj b*P.proj d*B)) :=
70         Matrix.trace_mul_comm _ _
71       _ = 0 := by
72         simp only [←Matrix.mul_assoc]
73         rw [P.mul_proj c a]
74         simp [hca]
75   · calc
76       Matrix.trace ((P.proj a*Aᴴ*P.proj b)*P.block B d c) =
77           Matrix.trace (P.proj a*Aᴴ*(P.proj b*P.proj d)*B*P.proj c) := by
78         simp only [PacketFamily.block,Matrix.mul_assoc]
79       _ = 0 := by
80         rw [P.mul_proj b d]
81         simp [hbd]
82 
83 theorem offDiagonal_trace_orthogonal (hP : ∀ a, (P.proj a)ᴴ = P.proj a)
84     (A : Matrix X X ℂ) (e f : I × I) (hne : e ≠ f) :
85     Matrix.trace ((offDiagonalTerm P A e)ᴴ * offDiagonalTerm P A f) = 0 := by
86   by_cases he : e.1=e.2
87   · simp [offDiagonalTerm,he]
88   · by_cases hf : f.1=f.2
89     · simp [offDiagonalTerm,hf]
90     · simp only [offDiagonalTerm,he,hf,ite_false]
91       exact block_trace_orthogonal P hP A A e.1 e.2 f.1 f.2 hne
92 
93 section Frobenius
94 open scoped Matrix.Norms.Frobenius
95 
96 /-- The actual Frobenius norm agrees with the Hilbert--Schmidt trace form. -/
97 theorem frobenius_sq_trace (A : Matrix X X ℂ) :
98     ‖A‖^2 = (Matrix.trace (Aᴴ*A)).re := by
99   rw [Matrix.frobenius_norm_def]
100   simp only [Real.rpow_two,←Real.sqrt_eq_rpow]
101   rw [Real.sq_sqrt (Finset.sum_nonneg (fun i _ => Finset.sum_nonneg
102     (fun j _ => sq_nonneg ‖A i j‖)))]
103   simp only [Matrix.trace,Matrix.diag,Matrix.mul_apply,Matrix.conjTranspose_apply,
104     Complex.re_sum,Complex.star_def,Complex.conj_mul',←Complex.ofReal_pow,Complex.ofReal_re]
105   exact Finset.sum_comm
106 
107 /-- Pythagoras from the trace expansion, with every cross term eliminated. -/
108 theorem frobenius_sum_sq {J : Type*} [Fintype J] [DecidableEq J]
109     (T : J → Matrix X X ℂ)
110     (hT : ∀ i j, i ≠ j → Matrix.trace ((T i)ᴴ*T j) = 0) :
111     ‖∑ j, T j‖^2 = ∑ j, ‖T j‖^2 := by
112   simp_rw [frobenius_sq_trace]
113   have ht : Matrix.trace ((∑ j,T j)ᴴ*(∑ j,T j)) =
114       ∑ j, Matrix.trace ((T j)ᴴ*T j) := by
115     simp only [Matrix.conjTranspose_sum,Matrix.sum_mul,Matrix.mul_sum,Matrix.trace_sum]
116     apply Finset.sum_congr rfl
117     intro i _
118     apply Finset.sum_eq_single i
119     · intro j _ hji
120       exact hT j i hji
121     · simp
122   rw [ht]
123   simp
124 
125 /-- Frobenius half of item 9.2, for arbitrary self-adjoint projectors. -/
126 theorem discovery_frobenius_certificate (hP : ∀ a, (P.proj a)ᴴ = P.proj a)
127     (A : Matrix X X ℂ) :
128     ‖A-diagonalCompression P A‖^2 =
129       ∑ b, ∑ a, if b=a then 0 else ‖P.block A b a‖^2 := by
130   rw [compression_residual P A,
131     frobenius_sum_sq (offDiagonalTerm P A) (offDiagonal_trace_orthogonal P hP A)]
132   simp only [Fintype.sum_prod_type,offDiagonalTerm]
133   apply Finset.sum_congr rfl
134   intro b _
135   apply Finset.sum_congr rfl
136   intro a _
137   by_cases h : b=a <;> simp [h]
138 end Frobenius
139 
140 section Operator
141 open scoped Matrix.Norms.L2Operator
142 
143 /-- Operator-norm half of item 9.2; this is the Euclidean induced matrix norm. -/
144 theorem discovery_operator_certificate (A : Matrix X X ℂ) :
145     ‖A-diagonalCompression P A‖ ≤
146       ∑ b, ∑ a, if b=a then 0 else ‖P.block A b a‖ := by
147   rw [compression_residual P A]
148   apply (norm_sum_le _ _).trans_eq
149   simp only [Fintype.sum_prod_type,offDiagonalTerm]
150   apply Finset.sum_congr rfl
151   intro b _
152   apply Finset.sum_congr rfl
153   intro a _
154   by_cases h : b=a <;> simp [h]
155 end Operator
156 
157 end KomorebiPaperVIII
158 
159 -- FIFTH BLOCK AXIOM AUDIT
160 #print axioms KomorebiPaperVIII.compression_decomposition
161 #print axioms KomorebiPaperVIII.compression_residual
162 #print axioms KomorebiPaperVIII.block_trace_orthogonal
163 #print axioms KomorebiPaperVIII.offDiagonal_trace_orthogonal
164 #print axioms KomorebiPaperVIII.frobenius_sq_trace
165 #print axioms KomorebiPaperVIII.frobenius_sum_sq
166 #print axioms KomorebiPaperVIII.discovery_frobenius_certificate
167 #print axioms KomorebiPaperVIII.discovery_operator_certificate
168 #print axioms KomorebiPaperVIII.diagonalCompression

Back to source controls