SmallCoreRecompression.lean

1 module
2 public import SpectralOptimality
3 public import FrobeniusOptimality
4 public import CompactTruncation
5 public import SmallCoreTransfer
6 import all SmallCoreNorms
7 import all CompactRangeFactors
8 import all SmallCoreTransfer
9 import all KernelFrame
10 import all DiagonalTruncation
11 import all SpectralOptimality
12 import all FrobeniusOptimality
13 import all CompactTruncation
14 public import Mathlib.Tactic
15 /-! Author: Komorebi P. Paper VIII, Theorem 5.6.
16 An ordered thin SVD is supplied by its algebraic equations, exactly as in the
17 manuscript's phrase "let G = W Sigma Z* be an SVD". No best-approximation,
18 singular-value tail, rank, norm invariance, or ambient optimality is assumed.
19 The construction of compact column bases is independent of this SVD datum.
20 These are exact finite matrices, not a floating-point QR or SVD implementation. -/
21 public section
22 set_option autoImplicit false
23 namespace KomorebiPaperVIII.SmallCore
24 open scoped BigOperators Matrix Classical Matrix.Norms.Frobenius
25 variable {m n r s t : Type*} [Fintype m] [Fintype n] [Fintype r] [Fintype s] [Fintype t]
26   [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] [DecidableEq t]
27   {d : ℕ}
28 
29 structure OrderedThinSVD (G : Matrix r s ℂ) (d : ℕ) where
30   left : Matrix r (Fin d) ℂ
31   right : Matrix s (Fin d) ℂ
32   values : Fin d → ℝ
33   left_isometry : leftᴴ*left=1
34   right_isometry : rightᴴ*right=1
35   nonnegative : ∀ i, 0 ≤ values i
36   sorted : Antitone values
37   reconstruction : G=lift left right (diag values)
38 
39 omit [DecidableEq m] in
40 theorem isometry_comp (Q : Matrix m r ℂ) (W : Matrix r (Fin d) ℂ)
41     (hQ : Qᴴ*Q=1) (hW : Wᴴ*W=1) : (Q*W)ᴴ*(Q*W)=1 := by
42   simp only [Matrix.conjTranspose_mul,Matrix.mul_assoc]
43   rw [←Matrix.mul_assoc Qᴴ Q W,hQ,Matrix.one_mul,hW]
44 
45 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
46     [DecidableEq r] [DecidableEq s] in
47 theorem lift_comp (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
48     (W : Matrix r (Fin d) ℂ) (Z : Matrix s (Fin d) ℂ)
49     (D : Matrix (Fin d) (Fin d) ℂ) :
50     lift Q V (lift W Z D)=lift (Q*W) (V*Z) D := by
51   simp only [lift,Matrix.conjTranspose_mul,Matrix.mul_assoc]
52 
53 omit [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
54 noncomputable def recompressLeft (Q : Matrix m r ℂ) {G : Matrix r s ℂ}
55     (svd : OrderedThinSVD G d) (k : ℕ) : Matrix m (KeptColumn d k) ℂ :=
56   Q*svd.left*rootMask svd.values k
57 
58 omit [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
59 noncomputable def recompressRight (V : Matrix n s ℂ) {G : Matrix r s ℂ}
60     (svd : OrderedThinSVD G d) (k : ℕ) : Matrix n (KeptColumn d k) ℂ :=
61   V*svd.right*rootMask svd.values k
62 
63 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] in
64 theorem recompressed_product (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
65     {G : Matrix r s ℂ} (svd : OrderedThinSVD G d) (k : ℕ) :
66     recompressLeft Q svd k * (recompressRight V svd k)ᴴ =
67       lift (Q*svd.left) (V*svd.right) (diag (kept svd.values k)) := by
68   exact thin_factor_product _ _ _ svd.nonnegative k
69 
70 omit [DecidableEq r] [DecidableEq s] in
71 /-- The core's singular-vector equations are derived from the SVD equations. -/
72 theorem core_gram_eigenvectors {G : Matrix r s ℂ} (svd : OrderedThinSVD G d) :
73     Gᴴ*G*svd.right = svd.right*diag (fun i => svd.values i ^ 2) := by
74   have hself : (diag svd.values)ᴴ = diag svd.values := by
75     simp [diag,Matrix.diagonal_conjTranspose]
76   have hsquare : diag svd.values*diag svd.values = diag (fun i => svd.values i^2) := by
77     simp only [diag,Matrix.diagonal_mul_diagonal]
78     congr 1
79     funext i
80     simp [pow_two]
81   calc
82     Gᴴ*G*svd.right = (lift svd.left svd.right (diag svd.values))ᴴ *
83         lift svd.left svd.right (diag svd.values) * svd.right :=
84       congrArg (fun X : Matrix r s ℂ => Xᴴ*X*svd.right) svd.reconstruction
85     _ = _ := by
86       simp only [lift,Matrix.conjTranspose_mul,Matrix.conjTranspose_conjTranspose,hself,Matrix.mul_assoc]
87       rw [←Matrix.mul_assoc svd.leftᴴ svd.left _,svd.left_isometry,Matrix.one_mul]
88       rw [svd.right_isometry,Matrix.mul_one,hsquare]
89 
90 /-- Both global optimality inequalities and exact errors, against arbitrary ambient competitors. -/
91 theorem recompression_optimality (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
92     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) {G : Matrix r s ℂ}
93     (svd : OrderedThinSVD G d) (k : ℕ) :
94     let A := lift Q V G
95     let B := recompressLeft Q svd k * (recompressRight V svd k)ᴴ
96     BestRank spectralNorm A B k ∧ BestRank frobeniusNorm A B k ∧
97     spectralNorm (A-B)=nextSingular svd.values k ∧
98     frobeniusNorm (A-B)^2=tailEnergy svd.values k ∧
99     frobeniusNorm (A-B)=Real.sqrt (tailEnergy svd.values k) := by
100   dsimp only
101   have hG : lift Q V G=lift (Q*svd.left) (V*svd.right) (diag svd.values) :=
102     (congrArg (lift Q V) svd.reconstruction).trans (lift_comp Q V _ _ _)
103   rw [recompressed_product,hG]
104   have hU := isometry_comp Q svd.left hQ svd.left_isometry
105   have hZ := isometry_comp V svd.right hV svd.right_isometry
106   have hs := spectral_best_lift (Q*svd.left) (V*svd.right) hU hZ _ _ k
107     (diagonal_spectral_best svd.values svd.nonnegative svd.sorted k)
108   have hf := frobenius_best_lift (Q*svd.left) (V*svd.right) hU hZ _ _ k
109     (diagonal_frobenius_best svd.values svd.nonnegative svd.sorted k)
110   refine ⟨hs,hf,?_,?_,?_⟩
111   · rw [←lift_sub,spectral_lift _ _ hU hZ,diagonal_residual]
112     exact spectral_diagonal_tail _ svd.nonnegative svd.sorted k
113   · rw [←lift_sub,frobenius_lift _ _ hU hZ,diagonal_residual]
114     exact frobenius_diagonal_tail _ k
115   · rw [←lift_sub,frobenius_lift _ _ hU hZ,diagonal_residual]
116     rw [←frobenius_diagonal_tail svd.values k,Real.sqrt_sq_eq_abs]
117     have hn : 0 ≤ frobeniusNorm (diag (discarded svd.values k)) := by
118       unfold frobeniusNorm
119       exact norm_nonneg (diag (discarded svd.values k))
120     exact (abs_of_nonneg hn).symm
121 
122 /-- Theorem 5.6 with independently constructed compact factors of the original inputs.
123 The output has min(d,k) columns, including k=0 and zero-rank factors. -/
124 theorem small_core_optimal_recompression (L : Matrix m t ℂ) (R : Matrix n t ℂ)
125     (svd : OrderedThinSVD (factorCore L R) d) (k : ℕ) :
126     let Lk := recompressLeft (compactQ L) svd k
127     let Rk := recompressRight (compactQ R) svd k
128     BestRank spectralNorm (L*Rᴴ) (Lk*Rkᴴ) k ∧
129     BestRank frobeniusNorm (L*Rᴴ) (Lk*Rkᴴ) k ∧
130     spectralNorm (L*Rᴴ-Lk*Rkᴴ)=nextSingular svd.values k ∧
131     frobeniusNorm (L*Rᴴ-Lk*Rkᴴ)^2=tailEnergy svd.values k ∧
132     frobeniusNorm (L*Rᴴ-Lk*Rkᴴ)=Real.sqrt (tailEnergy svd.values k) ∧
133     compactDim L=L.rank ∧ compactDim R=R.rank ∧
134     Fintype.card (KeptColumn d k)=min d k := by
135   dsimp only
136   have h := recompression_optimality (compactQ L) (compactQ R)
137     (compactQ_isometry L) (compactQ_isometry R) svd k
138   dsimp only at h
139   rw [←compact_product_reconstruction L R] at h
140   exact ⟨h.1,h.2.1,h.2.2.1,h.2.2.2.1,h.2.2.2.2,
141     compactDim_eq_rank L,compactDim_eq_rank R,keptColumn_card k⟩
142 
143 end KomorebiPaperVIII.SmallCore
144 
145 -- SIXTH AXIOM AUDITS
146 #print axioms KomorebiPaperVIII.SmallCore.isometry_comp
147 #print axioms KomorebiPaperVIII.SmallCore.lift_comp
148 #print axioms KomorebiPaperVIII.SmallCore.recompressed_product
149 #print axioms KomorebiPaperVIII.SmallCore.core_gram_eigenvectors
150 #print axioms KomorebiPaperVIII.SmallCore.recompression_optimality
151 #print axioms KomorebiPaperVIII.SmallCore.small_core_optimal_recompression
152 #print axioms KomorebiPaperVIII.SmallCore.OrderedThinSVD
153 #print axioms KomorebiPaperVIII.SmallCore.recompressLeft
154 #print axioms KomorebiPaperVIII.SmallCore.recompressRight

Back to source controls