KernelFrame.lean

1 module
2 public import SmallCoreNorms
3 import all SmallCoreNorms
4 public import Mathlib.Analysis.InnerProductSpace.PiL2
5 public import Mathlib.Analysis.InnerProductSpace.Subspace
6 public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
7 public import Mathlib.Tactic
8 /-! Author: Komorebi P. Orthonormal kernel coordinates and diagonal projection weights. -/
9 public section
10 set_option autoImplicit false
11 namespace KomorebiPaperVIII.SmallCore
12 open scoped BigOperators Matrix Classical
13 variable {n r : Type*} [Fintype n] [Fintype r] [DecidableEq n] [DecidableEq r]
14 noncomputable def subspaceFrame (S : Submodule ℂ (EuclideanSpace ℂ n)) :
15     Matrix n (Fin (Module.finrank ℂ S)) ℂ :=
16   LinearMap.toMatrix (stdOrthonormalBasis ℂ S).toBasis
17     (EuclideanSpace.basisFun n ℂ).toBasis S.subtype
18 
19 omit [DecidableEq n] in
20 theorem subspaceFrame_apply (S : Submodule ℂ (EuclideanSpace ℂ n))
21     (i : n) (j : Fin (Module.finrank ℂ S)) :
22     subspaceFrame S i j = (stdOrthonormalBasis ℂ S j : EuclideanSpace ℂ n) i := by
23   simp [subspaceFrame,LinearMap.toMatrix_apply]
24 
25 omit [DecidableEq n] in
26 theorem subspaceFrame_isometry (S : Submodule ℂ (EuclideanSpace ℂ n)) :
27     (subspaceFrame S)ᴴ * subspaceFrame S = 1 := by
28   ext i j
29   have h := orthonormal_iff_ite.mp (stdOrthonormalBasis ℂ S).orthonormal i j
30   simpa only [Submodule.coe_inner,PiLp.inner_apply,RCLike.inner_apply,
31     Matrix.mul_apply,Matrix.conjTranspose_apply,subspaceFrame_apply,Matrix.one_apply,
32     Complex.star_def,mul_comm] using h
33 
34 noncomputable def kernelSpace (B : Matrix n n ℂ) : Submodule ℂ (EuclideanSpace ℂ n) :=
35   LinearMap.ker (Matrix.toEuclideanLin B)
36 noncomputable def kernelDim (B : Matrix n n ℂ) := Module.finrank ℂ (kernelSpace B)
37 noncomputable def kernelFrame (B : Matrix n n ℂ) : Matrix n (Fin (kernelDim B)) ℂ :=
38   subspaceFrame (kernelSpace B)
39 
40 theorem kernelFrame_isometry (B : Matrix n n ℂ) : (kernelFrame B)ᴴ*kernelFrame B=1 :=
41   subspaceFrame_isometry _
42 
43 set_option backward.isDefEq.respectTransparency false in
44 theorem mul_kernelFrame (B : Matrix n n ℂ) : B*kernelFrame B=0 := by
45   unfold kernelFrame subspaceFrame
46   conv_lhs => lhs; rw [←LinearMap.toMatrix_toLin (EuclideanSpace.basisFun n ℂ).toBasis
47     (EuclideanSpace.basisFun n ℂ).toBasis B]
48   rw [←LinearMap.toMatrix_comp]
49   have he : Matrix.toLin (EuclideanSpace.basisFun n ℂ).toBasis
50       (EuclideanSpace.basisFun n ℂ).toBasis B ∘ₗ (kernelSpace B).subtype = 0 := by
51     ext x i
52     exact congrArg (fun z : EuclideanSpace ℂ n => z i) x.property
53   rw [he,map_zero]
54 
55 set_option backward.isDefEq.respectTransparency false in
56 theorem kernel_rank_nullity (B : Matrix n n ℂ) : B.rank+kernelDim B=Fintype.card n := by
57   have h := LinearMap.finrank_range_add_finrank_ker (Matrix.toEuclideanLin B)
58   have hr := Matrix.rank_eq_finrank_range_toLin B
59     (EuclideanSpace.basisFun n ℂ).toBasis (EuclideanSpace.basisFun n ℂ).toBasis
60   rw [←Matrix.toEuclideanLin_eq_toLin_orthonormal] at hr
61   simpa only [←hr,kernelSpace,kernelDim,finrank_euclideanSpace] using h
62 
63 noncomputable def rowWeight (Q : Matrix n r ℂ) (i : n) : ℝ := ∑ j, ‖Q i j‖^2
64 
65 omit [Fintype n] [DecidableEq n] [DecidableEq r] in
66 theorem rowWeight_nonneg (Q : Matrix n r ℂ) (i : n) : 0 ≤ rowWeight Q i :=
67   Finset.sum_nonneg (fun _ _ => sq_nonneg _)
68 
69 omit [DecidableEq n] in
70 theorem rowWeight_sum (Q : Matrix n r ℂ) (hQ : Qᴴ*Q=1) :
71     ∑ i, rowWeight Q i = Fintype.card r := by
72   have h : (Matrix.trace (Qᴴ*Q)).re = Fintype.card r := by simp [hQ]
73   have he : (Matrix.trace (Qᴴ*Q)).re = ∑ i, rowWeight Q i := by
74     simp only [rowWeight,Matrix.trace,Matrix.diag,Matrix.mul_apply,Matrix.conjTranspose_apply,
75       Complex.re_sum,Complex.star_def,Complex.conj_mul',←Complex.ofReal_pow,Complex.ofReal_re]
76     exact Finset.sum_comm
77   rw [he] at h
78   exact h
79 
80 section Operator
81 open scoped Matrix.Norms.L2Operator
82 /-- The diagonal weights of an orthogonal projection lie in [0,1]. -/
83 theorem rowWeight_le_one (Q : Matrix n r ℂ) (hQ : Qᴴ*Q=1) (i : n) : rowWeight Q i ≤ 1 := by
84   let x : EuclideanSpace ℂ n := WithLp.toLp 2 (Pi.single i (1:ℂ))
85   let y : EuclideanSpace ℂ r := (EuclideanSpace.equiv r ℂ).symm (Qᴴ *ᵥ x)
86   have hb : ‖Qᴴ‖ ≤ 1 := by rw [Matrix.l2_opNorm_conjTranspose]; exact spectral_isometry_bound Q hQ
87   have hn : ‖y‖ ≤ ‖Qᴴ‖ := by simpa [x,y] using Matrix.l2_opNorm_mulVec Qᴴ x
88   have he : ‖y‖^2 = rowWeight Q i := by
89     rw [EuclideanSpace.norm_sq_eq]
90     simp [y,x,rowWeight,Matrix.conjTranspose_apply]
91   nlinarith [norm_nonneg y]
92 
93 end Operator
94 end KomorebiPaperVIII.SmallCore
95 
96 -- SIXTH AXIOM AUDITS
97 #print axioms KomorebiPaperVIII.SmallCore.subspaceFrame_apply
98 #print axioms KomorebiPaperVIII.SmallCore.subspaceFrame_isometry
99 #print axioms KomorebiPaperVIII.SmallCore.kernelFrame_isometry
100 #print axioms KomorebiPaperVIII.SmallCore.mul_kernelFrame
101 #print axioms KomorebiPaperVIII.SmallCore.kernel_rank_nullity
102 #print axioms KomorebiPaperVIII.SmallCore.rowWeight_nonneg
103 #print axioms KomorebiPaperVIII.SmallCore.rowWeight_sum
104 #print axioms KomorebiPaperVIII.SmallCore.rowWeight_le_one
105 #print axioms KomorebiPaperVIII.SmallCore.kernelDim
106 #print axioms KomorebiPaperVIII.SmallCore.kernelFrame
107 #print axioms KomorebiPaperVIII.SmallCore.kernelSpace
108 #print axioms KomorebiPaperVIII.SmallCore.rowWeight
109 #print axioms KomorebiPaperVIII.SmallCore.subspaceFrame

Back to source controls