SpectralPseudoinverse.lean

1 import KomorebiLSM.SpectralLowerBound
2 import KomorebiLSM.NoisySubspaceResidual
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Spectral
6 open Komorebi.LSM.Identification
7 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
8 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
9 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
10 
11 theorem pinv_pointwise_bound (A : E →ₗ[ℝ] F)
12     (hr : 0 < Module.finrank ℝ A.range) (y : F) :
13     ‖pinv A y‖ ≤ (leastPositive A)⁻¹ * ‖y‖ := by
14   have hs := leastPositive_pos A hr
15   have h := lower_on_kernel_orthogonal A (pinv A y) (pinv_apply_mem A y)
16   rw [apply_pinv] at h
17   have h' := h.trans (A.range.norm_starProjection_apply_le y)
18   rw [inv_mul_eq_div]
19   exact (le_div_iff₀ hs).mpr (by simpa [mul_comm] using h')
20 
21 theorem pinv_operator_bound (A : E →L[ℝ] F)
22     (hr : 0 < Module.finrank ℝ A.toLinearMap.range) :
23     ‖pinvL A‖ ≤ (leastPositive A.toLinearMap)⁻¹ := by
24   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr (leastPositive_pos _ hr).le)
25   exact pinv_pointwise_bound A.toLinearMap hr
26 
27 /-- The inverse on the actual column space is constructed from the existing
28 orthogonal pseudoinverse, not postulated as input data. -/
29 noncomputable def rangeInverse (A : E →L[ℝ] F) : A.toLinearMap.range →L[ℝ] E :=
30   (pinvL A).comp A.toLinearMap.range.subtypeL
31 
32 theorem rangeInverse_right (A : E →L[ℝ] F) (x : A.toLinearMap.range) :
33     A (rangeInverse A x) = (x:F) := by
34   change A.toLinearMap (pinv A.toLinearMap (x:F)) = (x:F)
35   rw [apply_pinv, A.toLinearMap.range.starProjection_eq_self_iff.mpr x.property]
36 
37 theorem rangeInverse_bound (A : E →L[ℝ] F)
38     (hr : 0 < Module.finrank ℝ A.toLinearMap.range) :
39     ‖rangeInverse A‖ ≤ (leastPositive A.toLinearMap)⁻¹ := by
40   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr (leastPositive_pos _ hr).le)
41   intro x
42   exact pinv_pointwise_bound A.toLinearMap hr (x:F)
43 
44 /-- P32's inverse premise is now derived from the actual singular spectrum.
45 Only the estimated subspace's dimension and observed tail remain supplied. -/
46 theorem gap_from_observed_tail (X N : E →L[ℝ] F) (Q : Submodule ℝ F)
47     (hr : 0 < Module.finrank ℝ X.toLinearMap.range) (ε : ℝ) (hε : 0 ≤ ε)
48     (hsmall : ε < leastPositive X.toLinearMap / 2)
49     (htail : ‖Qᗮ.starProjection.comp (X+N)‖ ≤ ε) (hnoise : ‖N‖ ≤ ε)
50     (hdim : Module.finrank ℝ X.toLinearMap.range = Module.finrank ℝ Q) :
51     ‖X.toLinearMap.range.starProjection-Q.starProjection‖ ≤
52       2*ε/leastPositive X.toLinearMap ∧ 2*ε/leastPositive X.toLinearMap < 1 :=
53   OneSidedSubspace.two_epsilon_gap X.toLinearMap.range Q X N (rangeInverse X)
54     ε (leastPositive X.toLinearMap) hε (leastPositive_pos _ hr) hsmall htail hnoise
55     (rangeInverse_bound X hr) (rangeInverse_right X) hdim
56 
57 end Komorebi.LSM.Spectral

Back to source controls