SingularPerturbation.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 theorem exists_nonzero_intersection (P Q : Submodule ℝ E)
10     (hdim : Module.finrank ℝ E < Module.finrank ℝ P + Module.finrank ℝ Q) :
11     ∃ x : E, x ≠ 0 ∧ x ∈ P ∧ x ∈ Q := by
12   by_contra h
13   have hd : Disjoint P Q := Submodule.disjoint_def.mpr (by
14     intro x hx hy
15     by_contra hn
16     exact h ⟨x,hn,hx,hy⟩)
17   have hl := Submodule.finrank_add_finrank_le_of_disjoint hd
18   omega
19 
20 /-- Every ordered singular value changes by at most the operator perturbation.
21 This proof uses spectral subspaces and dimension intersection directly. -/
22 theorem singularValue_le_add_norm (A B : E →L[ℝ] F) (k : ℕ) :
23     A.toLinearMap.singularValues k ≤ B.toLinearMap.singularValues k + ‖A-B‖ := by
24   by_cases hk : k < Module.finrank ℝ E
25   · let P := rightHead A.toLinearMap (k+1) (by omega)
26     let Q := (rightHead B.toLinearMap k (by omega))ᗮ
27     have hp : Module.finrank ℝ P = k+1 := rightHead_finrank _ _ _
28     have hq : k + Module.finrank ℝ Q = Module.finrank ℝ E := by
29       have h := (rightHead B.toLinearMap k (show k ≤ Module.finrank ℝ E by omega)).finrank_add_finrank_orthogonal
30       rwa [rightHead_finrank] at h
31     obtain ⟨x,hx,hpx,hqx⟩ := exists_nonzero_intersection P Q (by omega)
32     have hl := lower_on_rightHead A.toLinearMap (k+1) (by omega) x hpx
33     simp only [Nat.add_sub_cancel] at hl
34     have hu := upper_on_rightTail B.toLinearMap k (by omega) x hqx
35     have hn := (A-B).le_opNorm x
36     have ht : ‖A x‖ ≤ ‖B x‖ + ‖(A-B) x‖ := by
37       have he : A x = B x + (A-B) x := by rw [sub_apply]; abel
38       rw [he]
39       exact norm_add_le _ _
40     have hxpos : 0 < ‖x‖ := norm_pos_iff.mpr hx
41     change A.toLinearMap.singularValues k * ‖x‖ ≤ ‖A x‖ at hl
42     change ‖B x‖ ≤ B.toLinearMap.singularValues k * ‖x‖ at hu
43     have hm : A.toLinearMap.singularValues k * ‖x‖ ≤
44         (B.toLinearMap.singularValues k + ‖A-B‖) * ‖x‖ := by nlinarith
45     exact (mul_le_mul_iff_left₀ hxpos).mp hm
46   · have hz : A.toLinearMap.singularValues k = 0 :=
47       A.toLinearMap.singularValues_eq_zero_iff_le_finrank_range.mpr
48         ((LinearMap.finrank_range_le A.toLinearMap).trans (by omega))
49     rw [hz]
50     exact add_nonneg (B.toLinearMap.singularValues_nonneg k) (norm_nonneg _)
51 
52 theorem singularValue_abs_sub_le (A B : E →L[ℝ] F) (k : ℕ) :
53     |A.toLinearMap.singularValues k - B.toLinearMap.singularValues k| ≤ ‖A-B‖ := by
54   have h₁ := singularValue_le_add_norm A B k
55   have h₂ := singularValue_le_add_norm B A k
56   rw [norm_sub_rev B A] at h₂
57   exact abs_le.mpr ⟨by linarith, by linarith⟩
58 
59 theorem noisy_singular_lower (X N : E →L[ℝ] F) (ε : ℝ) (hnoise : ‖N‖ ≤ ε)
60     (k : ℕ) : X.toLinearMap.singularValues k - ε ≤
61       (X+N).toLinearMap.singularValues k := by
62   have h := singularValue_le_add_norm X (X+N) k
63   have hn : ‖X-(X+N)‖ = ‖N‖ := by simp
64   rw [hn] at h
65   linarith
66 
67 theorem noisy_singular_upper (X N : E →L[ℝ] F) (ε : ℝ) (hnoise : ‖N‖ ≤ ε)
68     (k : ℕ) : (X+N).toLinearMap.singularValues k ≤
69       X.toLinearMap.singularValues k + ε := by
70   have h := singularValue_le_add_norm (X+N) X k
71   have hn : ‖X+N-X‖ = ‖N‖ := by simp
72   rw [hn] at h
73   linarith
74 
75 theorem noisy_tail_at_rank (X N : E →L[ℝ] F) (ε : ℝ) (hnoise : ‖N‖ ≤ ε) :
76     (X+N).toLinearMap.singularValues (Module.finrank ℝ X.toLinearMap.range) ≤ ε := by
77   have h := noisy_singular_upper X N ε hnoise (Module.finrank ℝ X.toLinearMap.range)
78   rw [X.toLinearMap.singularValues_finrank_range_self, zero_add] at h
79   exact h
80 
81 end Komorebi.LSM.Spectral

Back to source controls