RecompressionEndpoints.lean

1 module
2 public import SmallCoreRecompression
3 import all SmallCoreNorms
4 import all SmallCoreTransfer
5 import all CompactTruncation
6 import all DiagonalTruncation
7 import all SmallCoreRecompression
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Constructed SVD certificates and truncation endpoints.
10 This supplies nonvacuous zero/diagonal instances, not a general SVD algorithm. -/
11 public section
12 set_option autoImplicit false
13 namespace KomorebiPaperVIII.SmallCore
14 open scoped BigOperators Matrix Classical
15 variable {m n r s : Type*} [Fintype m] [Fintype n] [Fintype r] [Fintype s]
16   [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] {d : ℕ}
17 
18 noncomputable def diagonalSVD (σ : Fin d → ℝ) (hσ : ∀ i, 0 ≤ σ i)
19     (hsort : Antitone σ) : OrderedThinSVD (diag σ) d where
20   left := 1
21   right := 1
22   values := σ
23   left_isometry := by simp
24   right_isometry := by simp
25   nonnegative := hσ
26   sorted := hsort
27   reconstruction := by simp [lift]
28 
29 omit [DecidableEq r] [DecidableEq s] in
30 noncomputable def zeroSVD (G : Matrix r s ℂ) (hG : G=0) : OrderedThinSVD G 0 where
31   left := 0
32   right := 0
33   values := Fin.elim0
34   left_isometry := by ext i; exact i.elim0
35   right_isometry := by ext i; exact i.elim0
36   nonnegative := fun i => i.elim0
37   sorted := by intro i; exact i.elim0
38   reconstruction := by simp [lift,hG]
39 
40 theorem kept_zero (σ : Fin d → ℝ) : kept σ 0=0 := by
41   funext i
42   simp [kept]
43 
44 theorem kept_all (σ : Fin d → ℝ) (k : ℕ) (hk : d ≤ k) : kept σ k=σ := by
45   funext i
46   have hi : i.val<k := lt_of_lt_of_le i.isLt hk
47   simp [kept,hi]
48 
49 theorem tailEnergy_zero_of_full (σ : Fin d → ℝ) (k : ℕ) (hk : d ≤ k) :
50     tailEnergy σ k=0 := by
51   unfold tailEnergy
52   apply Finset.sum_eq_zero
53   intro i _
54   have hi : i.val<k := lt_of_lt_of_le i.isLt hk
55   simp [discarded,hi]
56 
57 theorem nextSingular_zero_of_full (σ : Fin d → ℝ) (k : ℕ) (hk : d ≤ k) :
58     nextSingular σ k=0 := by simp [nextSingular,not_lt_of_ge hk]
59 
60 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
61     [DecidableEq r] [DecidableEq s] in
62 theorem recompression_rank_zero (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
63     {G : Matrix r s ℂ} (svd : OrderedThinSVD G d) :
64     recompressLeft Q svd 0*(recompressRight V svd 0)ᴴ = 0 := by
65   rw [recompressed_product,kept_zero]
66   simp [lift,diag]
67 
68 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
69     [DecidableEq r] [DecidableEq s] in
70 theorem recompression_full (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
71     {G : Matrix r s ℂ} (svd : OrderedThinSVD G d) (k : ℕ) (hk : d ≤ k) :
72     recompressLeft Q svd k*(recompressRight V svd k)ᴴ = lift Q V G := by
73   rw [recompressed_product,kept_all _ k hk,←lift_comp]
74   exact congrArg (lift Q V) svd.reconstruction.symm
75 
76 end KomorebiPaperVIII.SmallCore
77 
78 -- SIXTH AXIOM AUDITS
79 #print axioms KomorebiPaperVIII.SmallCore.kept_zero
80 #print axioms KomorebiPaperVIII.SmallCore.kept_all
81 #print axioms KomorebiPaperVIII.SmallCore.tailEnergy_zero_of_full
82 #print axioms KomorebiPaperVIII.SmallCore.nextSingular_zero_of_full
83 #print axioms KomorebiPaperVIII.SmallCore.recompression_rank_zero
84 #print axioms KomorebiPaperVIII.SmallCore.recompression_full
85 #print axioms KomorebiPaperVIII.SmallCore.diagonalSVD
86 #print axioms KomorebiPaperVIII.SmallCore.zeroSVD

Back to source controls