LeftSingularModes.lean

1 import KomorebiLSM.SpectralTail
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 /-- Normalized image of a right singular mode; used only at positive singular values. -/
10 noncomputable def leftMode (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E)) : F :=
11   (A.singularValues i)⁻¹ • A (rightBasis A i)
12 
13 theorem singular_smul_leftMode (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E))
14     (hi : 0 < A.singularValues i) :
15     A.singularValues i • leftMode A i = A (rightBasis A i) := by
16   simp [leftMode, smul_smul, ne_of_gt hi]
17 
18 theorem leftMode_leftGram (A : E →ₗ[ℝ] F) (i : Fin (Module.finrank ℝ E)) :
19     (A.comp A.adjoint) (leftMode A i) = A.singularValues i^2 • leftMode A i := by
20   have hg := A.isSymmetric_adjoint_comp_self.apply_eigenvectorBasis rfl i
21   change A.adjoint (A (rightBasis A i)) = _ at hg
22   rw [← A.sq_singularValues_fin rfl i] at hg
23   simp only [leftMode, LinearMap.comp_apply, map_smul, hg]
24   rw [smul_comm]
25   simp [rightBasis]
26 
27 theorem leftModes_orthonormal (A : E →ₗ[ℝ] F) (k : ℕ)
28     (hk : k ≤ Module.finrank ℝ E) (hr : k ≤ Module.finrank ℝ A.range) :
29     Orthonormal ℝ (fun i : Fin k => leftMode A (Fin.castLE hk i)) := by
30   rw [orthonormal_iff_ite]
31   intro i j
32   have hi : A.singularValues (i:ℕ) ≠ 0 := ne_of_gt
33     (A.singularValues_pos_iff_lt_finrank_range.mpr (lt_of_lt_of_le i.isLt hr))
34   simp only [leftMode, inner_smul_left, inner_smul_right, conj_trivial,
35     image_inner, (rightBasis A).inner_eq_ite]
36   by_cases hij : i = j
37   · subst j
38     simp
39     field_simp [hi]
40   · have hne : Fin.castLE hk i ≠ Fin.castLE hk j :=
41       fun h => hij (Fin.castLE_injective hk h)
42     simp [hij, hne]
43 
44 /-- The constructed subspace is precisely the span of an orthonormal family of
45 left Gram eigenvectors with the first `k` ordered singular values. -/
46 theorem leadingLeft_eq_span_leftModes (A : E →ₗ[ℝ] F) (k : ℕ)
47     (hk : k ≤ Module.finrank ℝ E) (hr : k ≤ Module.finrank ℝ A.range) :
48     leadingLeft A k hk = Submodule.span ℝ
49       (Set.range (fun i : Fin k => leftMode A (Fin.castLE hk i))) := by
50   apply le_antisymm
51   · rintro y ⟨x,hx,rfl⟩
52     induction hx using Submodule.span_induction with
53     | mem x hx =>
54       obtain ⟨i,rfl⟩ := hx
55       rw [← singular_smul_leftMode A _
56         (A.singularValues_pos_iff_lt_finrank_range.mpr (lt_of_lt_of_le i.isLt hr))]
57       exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i,rfl⟩)
58     | zero => simp
59     | add x y hx hy ihx ihy => simpa using Submodule.add_mem _ ihx ihy
60     | smul a x hx ih => simpa using Submodule.smul_mem _ a ih
61   · apply Submodule.span_le.mpr
62     rintro _ ⟨i,rfl⟩
63     exact (leadingLeft A k hk).smul_mem _
64       ⟨_,basis_mem_rightHead A k hk _ i.isLt,rfl⟩
65 
66 end Komorebi.LSM.Spectral

Back to source controls