NoisySpectralSubspace.lean

1 import KomorebiLSM.SingularPerturbation
2 import KomorebiLSM.LeftSingularModes
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Spectral
6 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
8 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
9 
10 /-- Data-selected left subspace, with the true table's rank as truncation level. -/
11 noncomputable def learnedLeft (X N : E →L[ℝ] F) : Submodule ℝ F :=
12   leadingLeft (X+N).toLinearMap (Module.finrank ℝ X.toLinearMap.range)
13     (LinearMap.finrank_range_le X.toLinearMap)
14 
15 theorem noisy_rank_lower (X N : E →L[ℝ] F)
16     (hr : 0 < Module.finrank ℝ X.toLinearMap.range) (ε : ℝ)
17     (hnoise : ‖N‖ ≤ ε) (hsmall : ε < leastPositive X.toLinearMap / 2) :
18     Module.finrank ℝ X.toLinearMap.range ≤ Module.finrank ℝ (X+N).toLinearMap.range := by
19   have hl := noisy_singular_lower X N ε hnoise (Module.finrank ℝ X.toLinearMap.range-1)
20   have hp := leastPositive_pos X.toLinearMap hr
21   change leastPositive X.toLinearMap - ε ≤ _ at hl
22   have hy : 0 < (X+N).toLinearMap.singularValues (Module.finrank ℝ X.toLinearMap.range-1) := by
23     linarith
24   have hh := (X+N).toLinearMap.singularValues_pos_iff_lt_finrank_range.mp hy
25   omega
26 
27 theorem learnedLeft_finrank (X N : E →L[ℝ] F)
28     (hr : 0 < Module.finrank ℝ X.toLinearMap.range) (ε : ℝ)
29     (hnoise : ‖N‖ ≤ ε) (hsmall : ε < leastPositive X.toLinearMap / 2) :
30     Module.finrank ℝ (learnedLeft X N) = Module.finrank ℝ X.toLinearMap.range :=
31   leadingLeft_finrank _ _ _ (noisy_rank_lower X N hr ε hnoise hsmall)
32 
33 theorem learnedLeft_observed_tail (X N : E →L[ℝ] F) (ε : ℝ) (hnoise : ‖N‖ ≤ ε) :
34     ‖(learnedLeft X N)ᗮ.starProjection.comp (X+N)‖ ≤ ε := by
35   change ‖(leadingLeft (X+N).toLinearMap _ _)ᗮ.starProjection.comp (X+N)‖ ≤ ε
36   rw [leadingLeft_tail_norm]
37   exact noisy_tail_at_rank X N ε hnoise
38 
39 /-- The spectral and projection conclusions of P32 now follow from the noisy
40 operators alone. The estimated subspace and its tail are constructed. -/
41 theorem finite_table_stability (X N : E →L[ℝ] F)
42     (hr : 0 < Module.finrank ℝ X.toLinearMap.range) (ε : ℝ)
43     (hnoise : ‖N‖ ≤ ε) (hsmall : ε < leastPositive X.toLinearMap / 2) :
44     leastPositive X.toLinearMap - ε ≤
45       (X+N).toLinearMap.singularValues (Module.finrank ℝ X.toLinearMap.range-1) ∧
46     (X+N).toLinearMap.singularValues (Module.finrank ℝ X.toLinearMap.range) ≤ ε ∧
47     ‖X.toLinearMap.range.starProjection-(learnedLeft X N).starProjection‖ ≤
48       2*ε/leastPositive X.toLinearMap ∧
49     2*ε/leastPositive X.toLinearMap < 1 := by
50   have hε : 0 ≤ ε := (norm_nonneg N).trans hnoise
51   refine ⟨noisy_singular_lower X N ε hnoise _, noisy_tail_at_rank X N ε hnoise, ?_⟩
52   exact gap_from_observed_tail X N (learnedLeft X N) hr ε hε hsmall
53     (learnedLeft_observed_tail X N ε hnoise) hnoise
54     (learnedLeft_finrank X N hr ε hnoise hsmall).symm
55 
56 /-- The zero-padded spectrum also implements the maximum possible rank convention. -/
57 theorem singularValue_zero_at_max_rank (A : E →ₗ[ℝ] F) (k : ℕ)
58     (hk : min (Module.finrank ℝ E) (Module.finrank ℝ F) ≤ k) :
59     A.singularValues k = 0 := by
60   apply A.singularValues_eq_zero_iff_le_finrank_range.mpr
61   exact (le_min (LinearMap.finrank_range_le A) (Submodule.finrank_le A.range)).trans hk
62 
63 end Komorebi.LSM.Spectral

Back to source controls