SmallCoreTransfer.lean

1 module
2 public import CompactRangeFactors
3 import all SmallCoreNorms
4 import all CompactRangeFactors
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Optimality transfer for every ambient competitor.
7 The abstract transfer lemmas deliberately expose core optimality as a hypothesis;
8 the final SVD instantiation is a separate proof obligation. -/
9 public section
10 set_option autoImplicit false
11 namespace KomorebiPaperVIII.SmallCore
12 open scoped BigOperators Matrix Classical
13 variable {m n r s t : Type*} [Fintype m] [Fintype n] [Fintype r] [Fintype s] [Fintype t]
14   [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] [DecidableEq t]
15 
16 def BestRank (N : Matrix m n ℂ → ℝ) (A B : Matrix m n ℂ) (k : ℕ) : Prop :=
17   B.rank ≤ k ∧ ∀ C, C.rank ≤ k → N (A-B) ≤ N (A-C)
18 
19 omit [DecidableEq m] [DecidableEq n] in
20 theorem compressed_error (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
21     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G : Matrix r s ℂ) (B : Matrix m n ℂ) :
22     G-compress Q V B = compress Q V (lift Q V G - B) := by
23   rw [compress_sub,compress_lift Q V hQ hV]
24 
25 theorem spectral_best_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
26     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G H : Matrix r s ℂ) (k : ℕ)
27     (hbest : BestRank spectralNorm G H k) :
28     BestRank spectralNorm (lift Q V G) (lift Q V H) k := by
29   refine ⟨(rank_lift_le Q V H).trans hbest.1,fun B hB => ?_⟩
30   calc
31     spectralNorm (lift Q V G-lift Q V H) = spectralNorm (G-H) := by
32       rw [←lift_sub,spectral_lift Q V hQ hV]
33     _ ≤ spectralNorm (G-compress Q V B) := hbest.2 _ ((rank_compress_le Q V B).trans hB)
34     _ = spectralNorm (compress Q V (lift Q V G-B)) := by rw [compressed_error Q V hQ hV]
35     _ ≤ spectralNorm (lift Q V G-B) := spectral_compress_le Q V hQ hV _
36 
37 omit [DecidableEq m] [DecidableEq n] in
38 theorem frobenius_best_lift (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
39     (hQ : Qᴴ*Q=1) (hV : Vᴴ*V=1) (G H : Matrix r s ℂ) (k : ℕ)
40     (hbest : BestRank frobeniusNorm G H k) :
41     BestRank frobeniusNorm (lift Q V G) (lift Q V H) k := by
42   refine ⟨(rank_lift_le Q V H).trans hbest.1,fun B hB => ?_⟩
43   calc
44     frobeniusNorm (lift Q V G-lift Q V H) = frobeniusNorm (G-H) := by
45       rw [←lift_sub,frobenius_lift Q V hQ hV]
46     _ ≤ frobeniusNorm (G-compress Q V B) := hbest.2 _ ((rank_compress_le Q V B).trans hB)
47     _ = frobeniusNorm (compress Q V (lift Q V G-B)) := by rw [compressed_error Q V hQ hV]
48     _ ≤ frobeniusNorm (lift Q V G-B) := frobenius_compress_le Q V hQ hV _
49 
50 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] [DecidableEq t] in
51 theorem exact_factor_core (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
52     (RL : Matrix r t ℂ) (RR : Matrix s t ℂ) :
53     (Q*RL)*(V*RR)ᴴ = lift Q V (RL*RRᴴ) := by
54   simp only [lift,Matrix.conjTranspose_mul,Matrix.mul_assoc]
55 
56 omit [DecidableEq m] [DecidableEq n] in
57 noncomputable def factorCore (L : Matrix m t ℂ) (R : Matrix n t ℂ) :
58     Matrix (Fin (compactDim L)) (Fin (compactDim R)) ℂ := compactR L * (compactR R)ᴴ
59 
60 omit [DecidableEq m] [DecidableEq n] in
61 theorem compact_product_reconstruction (L : Matrix m t ℂ) (R : Matrix n t ℂ) :
62     L*Rᴴ = lift (compactQ L) (compactQ R) (factorCore L R) := by
63   calc
64     L*Rᴴ = (compactQ L*compactR L)*(compactQ R*compactR R)ᴴ := by
65       rw [compact_factorization,compact_factorization]
66     _ = _ := exact_factor_core _ _ _ _
67 
68 omit [DecidableEq m] [DecidableEq n] in
69 theorem compact_core_rank (L : Matrix m t ℂ) (R : Matrix n t ℂ) :
70     (factorCore L R).rank = (L*Rᴴ).rank := by
71   calc
72     (factorCore L R).rank = (lift (compactQ L) (compactQ R) (factorCore L R)).rank :=
73       (rank_lift _ _ (compactQ_isometry L) (compactQ_isometry R) _).symm
74     _ = _ := congrArg Matrix.rank (compact_product_reconstruction L R).symm
75 
76 omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [DecidableEq r] [DecidableEq s] [DecidableEq t] in
77 theorem factorized_truncation (Q : Matrix m r ℂ) (V : Matrix n s ℂ)
78     (U : Matrix r t ℂ) (Z : Matrix s t ℂ) (D : Matrix t t ℂ)
79     (hD : Dᴴ=D) (S : Matrix t t ℂ) (hS : D*D=S) :
80     (Q*U*D)*(V*Z*D)ᴴ = lift Q V (U*S*Zᴴ) := by
81   simp only [Matrix.conjTranspose_mul,hD,Matrix.mul_assoc,lift]
82   rw [←Matrix.mul_assoc D D (Zᴴ*Vᴴ),hS]
83 end KomorebiPaperVIII.SmallCore
84 
85 -- SIXTH AXIOM AUDITS
86 #print axioms KomorebiPaperVIII.SmallCore.compressed_error
87 #print axioms KomorebiPaperVIII.SmallCore.spectral_best_lift
88 #print axioms KomorebiPaperVIII.SmallCore.frobenius_best_lift
89 #print axioms KomorebiPaperVIII.SmallCore.exact_factor_core
90 #print axioms KomorebiPaperVIII.SmallCore.compact_product_reconstruction
91 #print axioms KomorebiPaperVIII.SmallCore.compact_core_rank
92 #print axioms KomorebiPaperVIII.SmallCore.factorized_truncation
93 #print axioms KomorebiPaperVIII.SmallCore.BestRank
94 #print axioms KomorebiPaperVIII.SmallCore.factorCore

Back to source controls