SpectralSubspaces.lean

1 import KomorebiLSM.SpectralSharpness
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Spectral
5 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
7 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
8 
9 /-- Span of the first `k` vectors of the ordered right Gram eigenbasis. -/
10 noncomputable def rightHead (A : E →ₗ[ℝ] F) (k : ℕ)
11     (hk : k ≤ Module.finrank ℝ E) : Submodule ℝ E :=
12   Submodule.span ℝ (Set.range (fun i : Fin k => rightBasis A (Fin.castLE hk i)))
13 
14 theorem rightHead_finrank (A : E →ₗ[ℝ] F) (k : ℕ)
15     (hk : k ≤ Module.finrank ℝ E) : Module.finrank ℝ (rightHead A k hk) = k := by
16   have hi : LinearIndependent ℝ (fun i : Fin k => rightBasis A (Fin.castLE hk i)) :=
17     (rightBasis A).orthonormal.linearIndependent.comp (Fin.castLE hk)
18       (Fin.castLE_injective hk)
19   exact (finrank_span_eq_card hi).trans (Fintype.card_fin k)
20 
21 theorem basis_mem_rightHead (A : E →ₗ[ℝ] F) (k : ℕ)
22     (hk : k ≤ Module.finrank ℝ E) (i : Fin (Module.finrank ℝ E)) (hi : (i:ℕ) < k) :
23     rightBasis A i ∈ rightHead A k hk := by
24   exact Submodule.subset_span ⟨⟨i,hi⟩, rfl⟩
25 
26 theorem rightHead_coordinate_zero (A : E →ₗ[ℝ] F) (k : ℕ)
27     (hk : k ≤ Module.finrank ℝ E) (x : E) (hx : x ∈ rightHead A k hk)
28     (i : Fin (Module.finrank ℝ E)) (hi : k ≤ (i:ℕ)) :
29     inner ℝ (rightBasis A i) x = 0 := by
30   induction hx using Submodule.span_induction with
31   | mem v hv =>
32     obtain ⟨j,rfl⟩ := hv
33     have hne : i ≠ Fin.castLE hk j := by
34       intro he
35       have := congrArg Fin.val he
36       have := j.isLt
37       simp only [Fin.val_castLE] at *
38       omega
39     exact (rightBasis A).orthonormal.2 hne
40   | zero => simp
41   | add x y hx hy ihx ihy => simp [inner_add_right, ihx, ihy]
42   | smul a x hx ih => simp [inner_smul_right, ih]
43 
44 theorem rightTail_coordinate_zero (A : E →ₗ[ℝ] F) (k : ℕ)
45     (hk : k ≤ Module.finrank ℝ E) (x : E) (hx : x ∈ (rightHead A k hk)ᗮ)
46     (i : Fin (Module.finrank ℝ E)) (hi : (i:ℕ) < k) :
47     inner ℝ (rightBasis A i) x = 0 :=
48   (rightHead A k hk).inner_right_of_mem_orthogonal (basis_mem_rightHead A k hk i hi) hx
49 
50 theorem lower_on_rightHead (A : E →ₗ[ℝ] F) (k : ℕ)
51     (hk : k ≤ Module.finrank ℝ E) (x : E) (hx : x ∈ rightHead A k hk) :
52     A.singularValues (k-1) * ‖x‖ ≤ ‖A x‖ := by
53   have hs := A.singularValues_nonneg (k-1)
54   have hsum : A.singularValues (k-1)^2 * ‖x‖^2 ≤ ‖A x‖^2 := by
55     rw [image_norm_sq, ← (rightBasis A).sum_sq_inner_right x, Finset.mul_sum]
56     apply Finset.sum_le_sum
57     intro i _
58     by_cases hi : (i:ℕ) < k
59     · have hle := A.singularValues_antitone (show (i:ℕ) ≤ k-1 by omega)
60       exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hs hle 2) (sq_nonneg _)
61     · rw [rightHead_coordinate_zero A k hk x hx i (by omega)]
62       simp
63   nlinarith [mul_pow (A.singularValues (k-1)) ‖x‖ 2,
64     mul_nonneg hs (norm_nonneg x), norm_nonneg (A x)]
65 
66 theorem upper_on_rightTail (A : E →ₗ[ℝ] F) (k : ℕ)
67     (hk : k ≤ Module.finrank ℝ E) (x : E) (hx : x ∈ (rightHead A k hk)ᗮ) :
68     ‖A x‖ ≤ A.singularValues k * ‖x‖ := by
69   have hs := A.singularValues_nonneg k
70   have hsum : ‖A x‖^2 ≤ A.singularValues k^2 * ‖x‖^2 := by
71     rw [image_norm_sq, ← (rightBasis A).sum_sq_inner_right x, Finset.mul_sum]
72     apply Finset.sum_le_sum
73     intro i _
74     by_cases hi : (i:ℕ) < k
75     · rw [rightTail_coordinate_zero A k hk x hx i hi]
76       simp
77     · have hle := A.singularValues_antitone (show k ≤ (i:ℕ) by omega)
78       exact mul_le_mul_of_nonneg_right
79         (pow_le_pow_left₀ (A.singularValues_nonneg _) hle 2) (sq_nonneg _)
80   nlinarith [mul_pow (A.singularValues k) ‖x‖ 2,
81     mul_nonneg hs (norm_nonneg x), norm_nonneg (A x)]
82 
83 theorem basis_mem_rightTail (A : E →ₗ[ℝ] F) (k : ℕ)
84     (hk : k ≤ Module.finrank ℝ E) (i : Fin (Module.finrank ℝ E)) (hi : k ≤ (i:ℕ)) :
85     rightBasis A i ∈ (rightHead A k hk)ᗮ := by
86   apply ((rightHead A k hk).mem_orthogonal' _).mpr
87   intro x hx
88   exact rightHead_coordinate_zero A k hk x hx i hi
89 
90 end Komorebi.LSM.Spectral

Back to source controls