SpectralTail.lean

1 import KomorebiLSM.SpectralSubspaces
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 /-- Actual left subspace generated by the images of the first right singular modes.
10 It has dimension `k` whenever `k` is at most the rank. -/
11 noncomputable def leadingLeft (A : E →ₗ[ℝ] F) (k : ℕ)
12     (hk : k ≤ Module.finrank ℝ E) : Submodule ℝ F :=
13   (rightHead A k hk).map A
14 
15 theorem rightHead_le_kernel_orthogonal (A : E →ₗ[ℝ] F) (k : ℕ)
16     (hk : k ≤ Module.finrank ℝ E) (hr : k ≤ Module.finrank ℝ A.range) :
17     rightHead A k hk ≤ A.kerᗮ := by
18   apply Submodule.span_le.mpr
19   rintro _ ⟨i,rfl⟩
20   exact positive_mode_orthogonal A _ (A.singularValues_pos_iff_lt_finrank_range.mpr
21     (lt_of_lt_of_le i.isLt hr))
22 
23 theorem leadingLeft_finrank (A : E →ₗ[ℝ] F) (k : ℕ)
24     (hk : k ≤ Module.finrank ℝ E) (hr : k ≤ Module.finrank ℝ A.range) :
25     Module.finrank ℝ (leadingLeft A k hk) = k := by
26   have hinj : Function.Injective (A.comp (rightHead A k hk).subtype) := by
27     apply LinearMap.ker_eq_bot.mp
28     apply le_antisymm _ bot_le
29     intro x hx
30     have hm : (x:E) ∈ A.ker := hx
31     have ho := rightHead_le_kernel_orthogonal A k hk hr x.property
32     have he : (x:E) = 0 := by
33       simpa using A.ker.inner_right_of_mem_orthogonal hm ho
34     change x = 0
35     exact Subtype.ext he
36   have h := LinearMap.finrank_range_of_inj hinj
37   rw [LinearMap.range_comp, Submodule.range_subtype, rightHead_finrank] at h
38   exact h
39 
40 theorem image_tail_orthogonal (A : E →ₗ[ℝ] F) (k : ℕ)
41     (hk : k ≤ Module.finrank ℝ E) (x : E) (hx : x ∈ (rightHead A k hk)ᗮ) :
42     A x ∈ (leadingLeft A k hk)ᗮ := by
43   intro y hy
44   obtain ⟨v,hv,rfl⟩ := hy
45   induction hv using Submodule.span_induction with
46   | mem v hv =>
47     obtain ⟨i,rfl⟩ := hv
48     rw [image_inner, rightTail_coordinate_zero A k hk x hx _ i.isLt, mul_zero]
49   | zero => simp
50   | add v w hv hw ihv ihw => simp [map_add, inner_add_left, ihv, ihw]
51   | smul a v hv ih => simp [map_smul, inner_smul_left, ih]
52 
53 theorem leadingLeft_residual_apply (A : E →ₗ[ℝ] F) (k : ℕ)
54     (hk : k ≤ Module.finrank ℝ E) (x : E) :
55     (leadingLeft A k hk)ᗮ.starProjection (A x) =
56       A ((rightHead A k hk)ᗮ.starProjection x) := by
57   have hsum := (rightHead A k hk).starProjection_add_starProjection_orthogonal x
58   have hm : A ((rightHead A k hk).starProjection x) ∈ leadingLeft A k hk :=
59     ⟨_,(rightHead A k hk).starProjection_apply_mem x,rfl⟩
60   have ho := image_tail_orthogonal A k hk _
61     ((rightHead A k hk)ᗮ.starProjection_apply_mem x)
62   conv_lhs => rw [← hsum, map_add, map_add]
63   rw [(leadingLeft A k hk).starProjection_orthogonal_apply_eq_zero hm,
64     (leadingLeft A k hk)ᗮ.starProjection_eq_self_iff.mpr ho, zero_add]
65 
66 theorem leadingLeft_tail_bound (A : E →L[ℝ] F) (k : ℕ)
67     (hk : k ≤ Module.finrank ℝ E) :
68     ‖(leadingLeft A.toLinearMap k hk)ᗮ.starProjection.comp A‖ ≤
69       A.toLinearMap.singularValues k := by
70   apply ContinuousLinearMap.opNorm_le_bound _ (A.toLinearMap.singularValues_nonneg k)
71   intro x
72   change ‖(leadingLeft A.toLinearMap k hk)ᗮ.starProjection (A.toLinearMap x)‖ ≤ _
73   rw [leadingLeft_residual_apply]
74   exact (upper_on_rightTail A.toLinearMap k hk _
75     ((rightHead A.toLinearMap k hk)ᗮ.starProjection_apply_mem x)).trans
76     (mul_le_mul_of_nonneg_left ((rightHead A.toLinearMap k hk)ᗮ.norm_starProjection_apply_le x)
77       (A.toLinearMap.singularValues_nonneg k))
78 
79 /-- The residual norm is exactly the next singular value, including a zero tail
80 when every domain direction is retained. -/
81 theorem leadingLeft_tail_norm (A : E →L[ℝ] F) (k : ℕ)
82     (hk : k ≤ Module.finrank ℝ E) :
83     ‖(leadingLeft A.toLinearMap k hk)ᗮ.starProjection.comp A‖ =
84       A.toLinearMap.singularValues k := by
85   apply le_antisymm (leadingLeft_tail_bound A k hk)
86   by_cases hlt : k < Module.finrank ℝ E
87   · let i : Fin (Module.finrank ℝ E) := ⟨k,hlt⟩
88     have h := ((leadingLeft A.toLinearMap k hk)ᗮ.starProjection.comp A).le_opNorm
89       (rightBasis A.toLinearMap i)
90     change ‖(leadingLeft A.toLinearMap k hk)ᗮ.starProjection
91       (A.toLinearMap (rightBasis A.toLinearMap i))‖ ≤ _ at h
92     rw [leadingLeft_residual_apply,
93       (rightHead A.toLinearMap k hk)ᗮ.starProjection_eq_self_iff.mpr
94         (basis_mem_rightTail A.toLinearMap k hk i le_rfl),
95       image_basis_norm, (rightBasis A.toLinearMap).norm_eq_one, mul_one] at h
96     exact h
97   · have hz : A.toLinearMap.singularValues k = 0 :=
98       A.toLinearMap.singularValues_eq_zero_iff_le_finrank_range.mpr
99         ((LinearMap.finrank_range_le A.toLinearMap).trans (by omega))
100     rw [hz]
101     exact norm_nonneg _
102 
103 end Komorebi.LSM.Spectral

Back to source controls