SmallCoreNorms.lean

1 module
2 public import Mathlib.Analysis.CStarAlgebra.Matrix
3 public import Mathlib.LinearAlgebra.Matrix.Rank
4 public import Mathlib.LinearAlgebra.Matrix.Trace
5 public import Mathlib.Tactic
6 
7 /-! Author: Komorebi P. Rectangular isometric embedding and compression.
8 All norms and ranks below are the actual matrix norms and rank.
9 No optimality or norm-preservation hypotheses are used. -/
10 public section
11 set_option autoImplicit false
12 namespace KomorebiPaperVIII.SmallCore
13 open scoped BigOperators Matrix Classical
14 variable {m n r s : Type*} [Fintype m] [Fintype n] [Fintype r] [Fintype s]
15   [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s]
16 
17 /-- Embed a small matrix into the ambient row and column spaces. -/
18 def lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (G : Matrix r s ℂ) : Matrix m n ℂ :=
19   Q * G * Vᴴ
20 /-- Compress an arbitrary ambient competitor into the small core. -/
21 def compress (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (B : Matrix m n ℂ) : Matrix r s ℂ :=
22   Qᴴ * B * V
23 
24 omit [DecidableEq m] [DecidableEq n] in
25 theorem compress_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
26     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G : Matrix r s ℂ) :
27     compress Q V (lift Q V G) = G := by
28   simp only [compress,lift,←Matrix.mul_assoc]
29   rw [hQ,Matrix.one_mul]
30   simp only [Matrix.mul_assoc,hV,Matrix.mul_one]
31 
32 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
33 theorem lift_sub (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (G H : Matrix r s ℂ) :
34     lift Q V (G-H) = lift Q V G - lift Q V H := by
35   simp only [lift,Matrix.mul_sub,Matrix.sub_mul]
36 
37 omit [Fintype r] [Fintype s] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
38 theorem compress_sub (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (A B : Matrix m n ℂ) :
39     compress Q V (A-B) = compress Q V A - compress Q V B := by
40   simp only [compress,Matrix.mul_sub,Matrix.sub_mul]
41 
42 omit [Fintype r] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
43 theorem rank_compress_le (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (B : Matrix m n ℂ) :
44     (compress Q V B).rank ≤ B.rank :=
45   (Matrix.rank_mul_le_left _ _).trans (Matrix.rank_mul_le_right _ _)
46 
47 omit [Fintype m] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
48 theorem rank_lift_le (Q : Matrix m r ℂ) (V : Matrix n s ℂ) (G : Matrix r s ℂ) :
49     (lift Q V G).rank ≤ G.rank :=
50   (Matrix.rank_mul_le_left _ _).trans (Matrix.rank_mul_le_right _ _)
51 
52 omit [DecidableEq m] [DecidableEq n] in
53 theorem rank_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
54     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G : Matrix r s ℂ) :
55     (lift Q V G).rank = G.rank := by
56   apply le_antisymm (rank_lift_le Q V G)
57   simpa only [compress_lift Q V hQ hV] using rank_compress_le Q V (lift Q V G)
58 
59 section Operator
60 open scoped Matrix.Norms.L2Operator
61 noncomputable def spectralNorm (A : Matrix m n ℂ) : ℝ := ‖A‖
62 
63 omit [DecidableEq m] in
64 theorem spectral_left_isometry (Q : Matrix m r ℂ) (hQ : Qᴴ*Q=1)
65     (G : Matrix r s ℂ) : ‖Q*G‖ = ‖G‖ := by
66   have he : (Q*G)ᴴ*(Q*G) = Gᴴ*G := by
67     simp only [Matrix.conjTranspose_mul,Matrix.mul_assoc]
68     rw [←Matrix.mul_assoc Qᴴ Q G,hQ,Matrix.one_mul]
69   have hn := congrArg (fun A : Matrix s s ℂ => ‖A‖) he
70   simp only [Matrix.l2_opNorm_conjTranspose_mul_self] at hn
71   nlinarith [norm_nonneg (Q*G),norm_nonneg G]
72 
73 theorem spectral_right_isometry (V : Matrix n s ℂ) (hV : Vᴴ*V=1)
74     (G : Matrix r s ℂ) : ‖G*Vᴴ‖ = ‖G‖ := by
75   calc
76     ‖G*Vᴴ‖ = ‖(G*Vᴴ)ᴴ‖ := (Matrix.l2_opNorm_conjTranspose _).symm
77     _ = ‖V*Gᴴ‖ := by simp only [Matrix.conjTranspose_mul,Matrix.conjTranspose_conjTranspose]
78     _ = ‖Gᴴ‖ := spectral_left_isometry V hV Gᴴ
79     _ = ‖G‖ := Matrix.l2_opNorm_conjTranspose _
80 
81 omit [DecidableEq m] in
82 theorem spectral_isometry_bound (Q : Matrix m r ℂ) (hQ : Qᴴ*Q=1) : ‖Q‖ ≤ 1 := by
83   have hn := Matrix.l2_opNorm_conjTranspose_mul_self Q
84   rw [hQ] at hn
85   have h1 : ‖(1 : Matrix r r ℂ)‖ ≤ 1 := by
86     rw [←Matrix.diagonal_one,Matrix.l2_opNorm_diagonal]
87     exact (pi_norm_le_iff_of_nonneg zero_le_one).mpr (fun i => by simp)
88   nlinarith [norm_nonneg Q]
89 
90 theorem spectral_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
91     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G : Matrix r s ℂ) :
92     spectralNorm (lift Q V G) = spectralNorm G := by
93   unfold spectralNorm lift
94   rw [spectral_right_isometry V hV,spectral_left_isometry Q hQ]
95 
96 theorem spectral_compress_le (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
97     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (B : Matrix m n ℂ) :
98     spectralNorm (compress Q V B) ≤ spectralNorm B := by
99   unfold spectralNorm compress
100   calc
101     ‖Qᴴ*B*V‖ ≤ ‖Qᴴ*B‖*‖V‖ := Matrix.l2_opNorm_mul _ _
102     _ ≤ (‖Qᴴ‖*‖B‖)*‖V‖ := mul_le_mul_of_nonneg_right (Matrix.l2_opNorm_mul _ _) (norm_nonneg _)
103     _ ≤ (1*‖B‖)*1 := by
104       apply mul_le_mul
105       · exact mul_le_mul_of_nonneg_right (by simpa only [Matrix.l2_opNorm_conjTranspose] using spectral_isometry_bound Q hQ) (norm_nonneg B)
106       · exact spectral_isometry_bound V hV
107       · exact norm_nonneg V
108       · positivity
109     _ = ‖B‖ := by ring
110 end Operator
111 
112 section Frobenius
113 open scoped Matrix.Norms.Frobenius
114 noncomputable def frobeniusNorm (A : Matrix m n ℂ) : ℝ := ‖A‖
115 
116 omit [DecidableEq m] [DecidableEq n] in
117 theorem frobenius_rect_sq_trace (A : Matrix m n ℂ) :
118     ‖A‖^2 = (Matrix.trace (Aᴴ*A)).re := by
119   rw [Matrix.frobenius_norm_def]
120   simp only [Real.rpow_two,←Real.sqrt_eq_rpow]
121   rw [Real.sq_sqrt (Finset.sum_nonneg (fun i _ => Finset.sum_nonneg
122     (fun j _ => sq_nonneg ‖A i j‖)))]
123   simp only [Matrix.trace,Matrix.diag,Matrix.mul_apply,Matrix.conjTranspose_apply,
124     Complex.re_sum,Complex.star_def,Complex.conj_mul',←Complex.ofReal_pow,Complex.ofReal_re]
125   exact Finset.sum_comm
126 
127 omit [DecidableEq m] [DecidableEq s] in
128 theorem frobenius_left_isometry (Q : Matrix m r ℂ) (hQ : Qᴴ*Q=1)
129     (G : Matrix r s ℂ) : ‖Q*G‖ = ‖G‖ := by
130   have he : (Q*G)ᴴ*(Q*G) = Gᴴ*G := by
131     simp only [Matrix.conjTranspose_mul,Matrix.mul_assoc]
132     rw [←Matrix.mul_assoc Qᴴ Q G,hQ,Matrix.one_mul]
133   have hn := congrArg (fun A : Matrix s s ℂ => (Matrix.trace A).re) he
134   rw [←frobenius_rect_sq_trace,←frobenius_rect_sq_trace] at hn
135   nlinarith [norm_nonneg (Q*G),norm_nonneg G]
136 
137 omit [DecidableEq n] [DecidableEq r] in
138 theorem frobenius_right_isometry (V : Matrix n s ℂ) (hV : Vᴴ*V=1)
139     (G : Matrix r s ℂ) : ‖G*Vᴴ‖ = ‖G‖ := by
140   calc
141     ‖G*Vᴴ‖ = ‖(G*Vᴴ)ᴴ‖ := (Matrix.frobenius_norm_conjTranspose _).symm
142     _ = ‖V*Gᴴ‖ := by simp only [Matrix.conjTranspose_mul,Matrix.conjTranspose_conjTranspose]
143     _ = ‖Gᴴ‖ := frobenius_left_isometry V hV Gᴴ
144     _ = ‖G‖ := Matrix.frobenius_norm_conjTranspose _
145 
146 omit [DecidableEq m] [DecidableEq n] in
147 /-- Orthogonal residual Pythagoras. The nonnegative discarded energy proves contraction. -/
148 theorem frobenius_projection_pythagoras (Q : Matrix m r ℂ) (hQ : Qᴴ*Q=1)
149     (B : Matrix m n ℂ) :
150     ‖B-Q*(Qᴴ*B)‖^2 = ‖B‖^2 - ‖Qᴴ*B‖^2 := by
151   have hleft : Bᴴ*(Q*(Qᴴ*B)) = (Qᴴ*B)ᴴ*(Qᴴ*B) := by
152     simp only [Matrix.conjTranspose_mul,Matrix.conjTranspose_conjTranspose,Matrix.mul_assoc]
153   have hright : (Q*(Qᴴ*B))ᴴ*B = (Qᴴ*B)ᴴ*(Qᴴ*B) := by
154     simp only [Matrix.conjTranspose_mul,Matrix.conjTranspose_conjTranspose,Matrix.mul_assoc]
155   have hlast : (Q*(Qᴴ*B))ᴴ*(Q*(Qᴴ*B)) = (Qᴴ*B)ᴴ*(Qᴴ*B) := by
156     simp only [Matrix.conjTranspose_mul,Matrix.mul_assoc]
157     rw [←Matrix.mul_assoc Qᴴ Q (Qᴴ*B),hQ,Matrix.one_mul]
158   simp only [frobenius_rect_sq_trace,Matrix.conjTranspose_sub,Matrix.sub_mul,Matrix.mul_sub,
159     hleft,hright,hlast,Matrix.trace_sub,Complex.sub_re]
160   ring
161 
162 omit [DecidableEq m] [DecidableEq n] in
163 theorem frobenius_left_compress_le (Q : Matrix m r ℂ) (hQ : Qᴴ*Q=1)
164     (B : Matrix m n ℂ) : ‖Qᴴ*B‖ ≤ ‖B‖ := by
165   have h := frobenius_projection_pythagoras Q hQ B
166   nlinarith [sq_nonneg ‖B-Q*(Qᴴ*B)‖, norm_nonneg (Qᴴ*B),norm_nonneg B]
167 
168 omit [DecidableEq m] [DecidableEq n] in
169 theorem frobenius_right_compress_le (V : Matrix n s ℂ) (hV : Vᴴ*V=1)
170     (B : Matrix m n ℂ) : ‖B*V‖ ≤ ‖B‖ := by
171   calc
172     ‖B*V‖ = ‖(B*V)ᴴ‖ := (Matrix.frobenius_norm_conjTranspose _).symm
173     _ = ‖Vᴴ*Bᴴ‖ := by rw [Matrix.conjTranspose_mul]
174     _ ≤ ‖Bᴴ‖ := frobenius_left_compress_le V hV Bᴴ
175     _ = ‖B‖ := Matrix.frobenius_norm_conjTranspose _
176 
177 omit [DecidableEq m] [DecidableEq n] in
178 theorem frobenius_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
179     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G : Matrix r s ℂ) :
180     frobeniusNorm (lift Q V G) = frobeniusNorm G := by
181   unfold frobeniusNorm lift
182   rw [frobenius_right_isometry V hV,frobenius_left_isometry Q hQ]
183 
184 omit [DecidableEq m] [DecidableEq n] in
185 theorem frobenius_compress_le (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
186     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (B : Matrix m n ℂ) :
187     frobeniusNorm (compress Q V B) ≤ frobeniusNorm B :=
188   (frobenius_right_compress_le V hV (Qᴴ*B)).trans (frobenius_left_compress_le Q hQ B)
189 end Frobenius
190 end KomorebiPaperVIII.SmallCore
191 
192 -- SIXTH AXIOM AUDITS
193 #print axioms KomorebiPaperVIII.SmallCore.compress_lift
194 #print axioms KomorebiPaperVIII.SmallCore.lift_sub
195 #print axioms KomorebiPaperVIII.SmallCore.compress_sub
196 #print axioms KomorebiPaperVIII.SmallCore.rank_compress_le
197 #print axioms KomorebiPaperVIII.SmallCore.rank_lift_le
198 #print axioms KomorebiPaperVIII.SmallCore.rank_lift
199 #print axioms KomorebiPaperVIII.SmallCore.spectral_left_isometry
200 #print axioms KomorebiPaperVIII.SmallCore.spectral_right_isometry
201 #print axioms KomorebiPaperVIII.SmallCore.spectral_isometry_bound
202 #print axioms KomorebiPaperVIII.SmallCore.spectral_lift
203 #print axioms KomorebiPaperVIII.SmallCore.spectral_compress_le
204 #print axioms KomorebiPaperVIII.SmallCore.frobenius_rect_sq_trace
205 #print axioms KomorebiPaperVIII.SmallCore.frobenius_left_isometry
206 #print axioms KomorebiPaperVIII.SmallCore.frobenius_right_isometry
207 #print axioms KomorebiPaperVIII.SmallCore.frobenius_projection_pythagoras
208 #print axioms KomorebiPaperVIII.SmallCore.frobenius_left_compress_le
209 #print axioms KomorebiPaperVIII.SmallCore.frobenius_right_compress_le
210 #print axioms KomorebiPaperVIII.SmallCore.frobenius_lift
211 #print axioms KomorebiPaperVIII.SmallCore.frobenius_compress_le
212 #print axioms KomorebiPaperVIII.SmallCore.compress
213 #print axioms KomorebiPaperVIII.SmallCore.frobeniusNorm
214 #print axioms KomorebiPaperVIII.SmallCore.lift
215 #print axioms KomorebiPaperVIII.SmallCore.spectralNorm

Back to source controls