SpectralOptimality.lean

1 module
2 public import DiagonalTruncation
3 public import KernelFrame
4 import all SmallCoreNorms
5 import all DiagonalTruncation
6 import all SmallCoreTransfer
7 public import Mathlib.Tactic
8 /-! Author: Komorebi P. Spectral low-rank lower bound by a prefix-kernel witness.
9 No Eckart--Young theorem or low-rank lower bound is assumed. -/
10 public section
11 set_option autoImplicit false
12 namespace KomorebiPaperVIII.SmallCore
13 open scoped BigOperators Matrix Classical
14 variable {d : ℕ}
15 
16 noncomputable def prefixEmbedding (k : ℕ) (hk : k+1≤d) :
17     Matrix (Fin d) (Fin (k+1)) ℂ :=
18   fun i j => if i=Fin.castLE hk j then 1 else 0
19 
20 theorem prefix_isometry (k : ℕ) (hk : k+1≤d) :
21     (prefixEmbedding k hk)ᴴ * prefixEmbedding k hk = 1 := by
22   ext i j
23   simp [prefixEmbedding,Matrix.mul_apply,Matrix.conjTranspose_apply,Matrix.one_apply,eq_comm]
24 
25 theorem prefix_support (k : ℕ) (hk : k+1≤d) (z : Fin (k+1) → ℂ)
26     (i : Fin d) (hi : k+1 ≤ i.val) : (prefixEmbedding k hk *ᵥ z) i = 0 := by
27   simp only [Matrix.mulVec,dotProduct]
28   apply Finset.sum_eq_zero
29   intro j _
30   have hne : i ≠ Fin.castLE hk j := by
31     intro he
32     have hv : i.val=j.val := by simpa using congrArg Fin.val he
33     have := j.isLt
34     omega
35   simp [prefixEmbedding,hne]
36 
37 set_option backward.isDefEq.respectTransparency false in
38 theorem rank_lt_kernel_witness {m n : Type*} [Fintype m] [Fintype n]
39     [DecidableEq m] [DecidableEq n] (B : Matrix m n ℂ) (hB : B.rank < Fintype.card n) :
40     ∃ z : EuclideanSpace ℂ n, z≠0 ∧ B*ᵥ z=0 := by
41   let f := Matrix.toEuclideanLin B
42   have hr := Matrix.rank_eq_finrank_range_toLin B
43     (EuclideanSpace.basisFun m ℂ).toBasis (EuclideanSpace.basisFun n ℂ).toBasis
44   rw [←Matrix.toEuclideanLin_eq_toLin_orthonormal] at hr
45   have hn := f.finrank_range_add_finrank_ker
46   have hp : 0 < Module.finrank ℂ f.ker := by
47     rw [←hr,finrank_euclideanSpace] at hn
48     omega
49   have hker : f.ker ≠ ⊥ := Submodule.one_le_finrank_iff.mp hp
50   obtain ⟨z,hz,hne⟩ := f.ker.ne_bot_iff.mp hker
51   refine ⟨z,hne,?_⟩
52   exact congrArg WithLp.ofLp hz
53 
54 /-- A rank-k matrix has a nonzero kernel vector supported in the first k+1 coordinates. -/
55 theorem prefix_kernel_witness (k : ℕ) (hk : k<d)
56     (B : Matrix (Fin d) (Fin d) ℂ) (hB : B.rank≤k) :
57     ∃ y : EuclideanSpace ℂ (Fin d), y≠0 ∧ B*ᵥ y=0 ∧
58       ∀ i : Fin d, k+1 ≤ i.val → y i=0 := by
59   let J := prefixEmbedding k (by omega : k+1≤d)
60   have hj : Jᴴ*J=1 := prefix_isometry k _
61   have hr : (B*J).rank < Fintype.card (Fin (k+1)) := by
62     have := Matrix.rank_mul_le_left B J
63     simp only [Fintype.card_fin]
64     omega
65   obtain ⟨z,hz,hbz⟩ := rank_lt_kernel_witness (B*J) hr
66   let y : EuclideanSpace ℂ (Fin d) := WithLp.toLp 2 (J*ᵥ z)
67   have hy : y≠0 := by
68     intro he
69     have he' : J*ᵥ z=0 := congrArg WithLp.ofLp he
70     have hz' : (z : Fin (k+1) → ℂ)=0 := by
71       calc
72         (z : Fin (k+1) → ℂ) = (Jᴴ*J)*ᵥ z := by rw [hj,Matrix.one_mulVec]
73         _ = Jᴴ*ᵥ(J*ᵥ z) := (Matrix.mulVec_mulVec _ _ _).symm
74         _ = 0 := by rw [he',Matrix.mulVec_zero]
75     apply hz
76     exact (EuclideanSpace.equiv (Fin (k+1)) ℂ).injective hz'
77   refine ⟨y,hy,?_,?_⟩
78   · change B*ᵥ(J*ᵥ z)=0
79     rw [Matrix.mulVec_mulVec]
80     exact hbz
81   · intro i hi
82     exact prefix_support k _ z i hi
83 
84 section Operator
85 open scoped Matrix.Norms.L2Operator
86 
87 theorem prefix_diagonal_lower (σ : Fin d → ℝ) (hσ : ∀ i, 0≤σ i)
88     (hsort : Antitone σ) (k : ℕ) (hk : k<d) (y : EuclideanSpace ℂ (Fin d))
89     (hy : ∀ i : Fin d, k+1 ≤ i.val → y i=0) :
90     σ ⟨k,hk⟩ * ‖y‖ ≤ ‖WithLp.toLp 2 (diag σ*ᵥ y)‖ := by
91   apply (sq_le_sq₀ (mul_nonneg (hσ _) (norm_nonneg y)) (norm_nonneg _)).mp
92   rw [mul_pow,EuclideanSpace.norm_sq_eq,EuclideanSpace.norm_sq_eq,Finset.mul_sum]
93   apply Finset.sum_le_sum
94   intro i _
95   by_cases hi : i.val<k+1
96   · have hle : σ ⟨k,hk⟩ ≤ σ i := hsort (by show i.val ≤ k; omega)
97     have hs : σ ⟨k,hk⟩^2 ≤ σ i^2 := by nlinarith [hσ i,hσ ⟨k,hk⟩]
98     simpa [diag,Matrix.mulVec_diagonal,norm_mul,mul_pow,Complex.norm_real,
99       Real.norm_eq_abs,sq_abs] using mul_le_mul_of_nonneg_right hs (sq_nonneg ‖y i‖)
100   · have hz := hy i (by omega)
101     simp [diag,Matrix.mulVec_diagonal,hz]
102 
103 theorem diagonal_spectral_lower (σ : Fin d → ℝ) (hσ : ∀ i, 0≤σ i)
104     (hsort : Antitone σ) (k : ℕ) (B : Matrix (Fin d) (Fin d) ℂ) (hB : B.rank≤k) :
105     nextSingular σ k ≤ spectralNorm (diag σ-B) := by
106   by_cases hk : k<d
107   · obtain ⟨y,hy,hby,hys⟩ := prefix_kernel_witness k hk B hB
108     have hl := prefix_diagonal_lower σ hσ hsort k hk y hys
109     have hu := Matrix.l2_opNorm_mulVec (diag σ-B) y
110     have he : (diag σ-B)*ᵥ y=diag σ*ᵥ y := by rw [Matrix.sub_mulVec,hby,sub_zero]
111     rw [he] at hu
112     have hle : σ ⟨k,hk⟩ * ‖y‖ ≤ ‖diag σ-B‖ * ‖y‖ := hl.trans hu
113     have hp : 0<‖y‖ := norm_pos_iff.mpr hy
114     have hb : σ ⟨k,hk⟩ ≤ ‖diag σ-B‖ := by nlinarith
115     simpa [nextSingular,hk,spectralNorm] using hb
116   · simp only [nextSingular,hk]
117     unfold spectralNorm
118     positivity
119 
120 theorem diagonal_spectral_best (σ : Fin d → ℝ) (hσ : ∀ i, 0≤σ i)
121     (hsort : Antitone σ) (k : ℕ) :
122     BestRank spectralNorm (diag σ) (diag (kept σ k)) k := by
123   refine ⟨rank_kept_le σ k,fun B hB => ?_⟩
124   rw [diagonal_residual,spectral_diagonal_tail σ hσ hsort]
125   exact diagonal_spectral_lower σ hσ hsort k B hB
126 end Operator
127 end KomorebiPaperVIII.SmallCore
128 
129 -- SIXTH AXIOM AUDITS
130 #print axioms KomorebiPaperVIII.SmallCore.prefix_isometry
131 #print axioms KomorebiPaperVIII.SmallCore.prefix_support
132 #print axioms KomorebiPaperVIII.SmallCore.rank_lt_kernel_witness
133 #print axioms KomorebiPaperVIII.SmallCore.prefix_kernel_witness
134 #print axioms KomorebiPaperVIII.SmallCore.prefix_diagonal_lower
135 #print axioms KomorebiPaperVIII.SmallCore.diagonal_spectral_lower
136 #print axioms KomorebiPaperVIII.SmallCore.diagonal_spectral_best
137 #print axioms KomorebiPaperVIII.SmallCore.prefixEmbedding

Back to source controls