FiniteTableP32.lean

1 import KomorebiLSM.DecoderMatrixFormula
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.FiniteTableP32
5 open Komorebi.LSM.Spectral Komorebi.LSM.BasisCoordinates
6 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
8 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
9 
10 /-- P32's basis conditioning, coordinate injection, exact inverse and inverse norm,
11 for any orthonormal bases of the true and data-selected ranges. The spectral and
12 projection assertions are `Spectral.finite_table_stability`; the literal matrix
13 formula is `BasisCoordinates.decoder_matrix_formula`. -/
14 theorem coordinates_and_decoder (X N : E →L[ℝ] F)
15     (hr : 0 < Module.finrank ℝ X.toLinearMap.range) (ε : ℝ)
16     (hnoise : ‖N‖ ≤ ε) (hsmall : ε < leastPositive X.toLinearMap / 2)
17     (U : OrthonormalBasis (Fin (Module.finrank ℝ X.toLinearMap.range)) ℝ X.toLinearMap.range)
18     (V : OrthonormalBasis (Fin (Module.finrank ℝ X.toLinearMap.range)) ℝ (learnedLeft X N)) :
19     Real.sqrt (1-(2*ε/leastPositive X.toLinearMap)^2) ≤
20       (cross U V).toEuclideanLin.singularValues (Module.finrank ℝ X.toLinearMap.range-1) ∧
21     Function.Injective ((coordinates V).comp X.toLinearMap.range.subtypeL) ∧
22     (∀ x : X.toLinearMap.range, decoder U V (coordinates V (x:F)) = (x:F)) ∧
23     (∀ y : EuclideanSpace ℝ (Fin (Module.finrank ℝ X.toLinearMap.range)),
24       coordinates V (decoder U V y) = y) ∧
25     ‖decoder U V‖ ≤ (Real.sqrt (1-(2*ε/leastPositive X.toLinearMap)^2))⁻¹ := by
26   obtain ⟨_,_,hg,hs⟩ := finite_table_stability X N hr ε hnoise hsmall
27   have hε : 0 ≤ ε := (norm_nonneg N).trans hnoise
28   have hδ : 0 ≤ 2*ε/leastPositive X.toLinearMap :=
29     div_nonneg (mul_nonneg (by norm_num) hε) (leastPositive_pos X.toLinearMap hr).le
30   exact ⟨cross_min_singular U V hr _ hδ hs hg,
31     coordinates_injective V _ hδ hs hg,
32     decoder_coordinates U V _ hδ hs hg,
33     coordinates_decoder U V _ hδ hs hg,
34     decoder_norm_bound U V _ hδ hs hg⟩
35 
36 end Komorebi.LSM.FiniteTableP32

Back to source controls