CompactRangeFactors.lean

1 module
2 public import SmallCoreNorms
3 public import Mathlib.Analysis.InnerProductSpace.PiL2
4 public import Mathlib.Analysis.InnerProductSpace.Subspace
5 public import Mathlib.Analysis.InnerProductSpace.Adjoint
6 public import Mathlib.Tactic
7 
8 /-! Author: Komorebi P. Actual compact orthonormal column-space factorization.
9 This is exact mathematics, not a floating-point QR implementation. -/
10 public section
11 set_option autoImplicit false
12 namespace KomorebiPaperVIII.SmallCore
13 open scoped BigOperators Matrix Classical
14 variable {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
15 
16 noncomputable def columnSpace (A : Matrix m n ℂ) : Submodule ℂ (EuclideanSpace ℂ m) :=
17   LinearMap.range (Matrix.toEuclideanLin A)
18 noncomputable def compactDim (A : Matrix m n ℂ) : ℕ := Module.finrank ℂ (columnSpace A)
19 noncomputable def columnBasis (A : Matrix m n ℂ) :
20     OrthonormalBasis (Fin (compactDim A)) ℂ (columnSpace A) :=
21   stdOrthonormalBasis ℂ (columnSpace A)
22 noncomputable def compactQ (A : Matrix m n ℂ) : Matrix m (Fin (compactDim A)) ℂ :=
23   LinearMap.toMatrix (columnBasis A).toBasis (EuclideanSpace.basisFun m ℂ).toBasis
24     (columnSpace A).subtype
25 noncomputable def compactR (A : Matrix m n ℂ) : Matrix (Fin (compactDim A)) n ℂ :=
26   LinearMap.toMatrix (EuclideanSpace.basisFun n ℂ).toBasis (columnBasis A).toBasis
27     (Matrix.toEuclideanLin A).rangeRestrict
28 
29 omit [DecidableEq m] in
30 theorem compactDim_eq_rank (A : Matrix m n ℂ) : compactDim A = A.rank := by
31   unfold compactDim columnSpace
32   rw [Matrix.toEuclideanLin_eq_toLin_orthonormal]
33   exact (Matrix.rank_eq_finrank_range_toLin A
34     (EuclideanSpace.basisFun m ℂ).toBasis (EuclideanSpace.basisFun n ℂ).toBasis).symm
35 
36 omit [DecidableEq m] in
37 theorem compactQ_apply (A : Matrix m n ℂ) (i : m) (j : Fin (compactDim A)) :
38     compactQ A i j = (columnBasis A j : EuclideanSpace ℂ m) i := by
39   simp [compactQ,LinearMap.toMatrix_apply]
40 
41 omit [DecidableEq m] in
42 theorem compactQ_isometry (A : Matrix m n ℂ) : (compactQ A)ᴴ*compactQ A = 1 := by
43   ext i j
44   have h := orthonormal_iff_ite.mp (columnBasis A).orthonormal i j
45   simpa only [Submodule.coe_inner,PiLp.inner_apply,RCLike.inner_apply,
46     Matrix.mul_apply,Matrix.conjTranspose_apply,compactQ_apply,Matrix.one_apply,
47     Complex.star_def,mul_comm] using h
48 
49 omit [DecidableEq m] in
50 set_option backward.isDefEq.respectTransparency false in
51 theorem compact_factorization (A : Matrix m n ℂ) : compactQ A * compactR A = A := by
52   unfold compactQ compactR
53   rw [←LinearMap.toMatrix_comp]
54   have he : (columnSpace A).subtype ∘ₗ (Matrix.toEuclideanLin A).rangeRestrict =
55       Matrix.toEuclideanLin A := by ext x i; rfl
56   rw [he,Matrix.toEuclideanLin_eq_toLin_orthonormal]
57   exact LinearMap.toMatrix_toLin _ _ _
58 
59 omit [DecidableEq m] in
60 theorem compactR_is_compression (A : Matrix m n ℂ) : compactR A = (compactQ A)ᴴ*A := by
61   calc
62     compactR A = (compactQ A)ᴴ*(compactQ A*compactR A) := by
63       rw [←Matrix.mul_assoc,compactQ_isometry,Matrix.one_mul]
64     _ = (compactQ A)ᴴ*A := congrArg (fun B => (compactQ A)ᴴ*B) (compact_factorization A)
65 
66 omit [DecidableEq m] in
67 theorem compactR_full_row_rank (A : Matrix m n ℂ) :
68     (compactR A).rank = compactDim A := by
69   apply le_antisymm
70   · simpa only [Fintype.card_fin] using Matrix.rank_le_card_height (compactR A)
71   · calc
72       compactDim A = A.rank := compactDim_eq_rank A
73       _ = (compactQ A * compactR A).rank := congrArg Matrix.rank (compact_factorization A).symm
74       _ ≤ (compactR A).rank := Matrix.rank_mul_le_right _ _
75 
76 omit [DecidableEq m] in
77 theorem compact_rank_zero (A : Matrix m n ℂ) : compactDim A = 0 ↔ A = 0 := by
78   constructor
79   · intro h
80     let : IsEmpty (Fin (compactDim A)) := ⟨fun i => by have := i.isLt; omega⟩
81     calc
82       A = compactQ A * compactR A := (compact_factorization A).symm
83       _ = 0 := by ext i j; simp [Matrix.mul_apply]
84   · intro h
85     simp [compactDim_eq_rank,h]
86 
87 end KomorebiPaperVIII.SmallCore
88 
89 -- SIXTH AXIOM AUDITS
90 #print axioms KomorebiPaperVIII.SmallCore.compactDim_eq_rank
91 #print axioms KomorebiPaperVIII.SmallCore.compactQ_apply
92 #print axioms KomorebiPaperVIII.SmallCore.compactQ_isometry
93 #print axioms KomorebiPaperVIII.SmallCore.compact_factorization
94 #print axioms KomorebiPaperVIII.SmallCore.compactR_is_compression
95 #print axioms KomorebiPaperVIII.SmallCore.compactR_full_row_rank
96 #print axioms KomorebiPaperVIII.SmallCore.compact_rank_zero
97 #print axioms KomorebiPaperVIII.SmallCore.columnBasis
98 #print axioms KomorebiPaperVIII.SmallCore.columnSpace
99 #print axioms KomorebiPaperVIII.SmallCore.compactDim
100 #print axioms KomorebiPaperVIII.SmallCore.compactQ
101 #print axioms KomorebiPaperVIII.SmallCore.compactR

Back to source controls