BasisCoordinates.lean

1 import KomorebiLSM.NoisySpectralSubspace
2 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.BasisCoordinates
6 open Komorebi.LSM.SubspaceCoordinates
7 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
8 variable [NormedAddCommGroup F] [InnerProductSpace ℝ F]
9 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F]
10 variable {r s : ℕ}
11 
12 omit [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] in
13 theorem matrix_action (U : OrthonormalBasis (Fin r) ℝ E)
14     (V : OrthonormalBasis (Fin s) ℝ F) (T : E →ₗ[ℝ] F)
15     (y : EuclideanSpace ℝ (Fin r)) :
16     (LinearMap.toMatrix U.toBasis V.toBasis T).toEuclideanLin y =
17       V.repr (T (U.repr.symm y)) := by
18   have h := T.toMatrix_mulVec_repr U.toBasis V.toBasis (U.repr.symm y)
19   ext i
20   have he : (U.toBasis.repr (U.repr.symm y) : Fin r → ℝ) = WithLp.ofLp y := by
21     funext j
22     simp
23   rw [he] at h
24   simpa using congrFun h i
25 
26 variable {P Q : Submodule ℝ E}
27 
28 /-- The matrix whose entries are the inner products of estimated and true basis
29 vectors: in ambient Euclidean coordinates this is `Uhatᵀ U`. -/
30 noncomputable def cross (U : OrthonormalBasis (Fin r) ℝ P)
31     (V : OrthonormalBasis (Fin r) ℝ Q) : Matrix (Fin r) (Fin r) ℝ :=
32   LinearMap.toMatrix U.toBasis V.toBasis (project P Q).toLinearMap
33 
34 /-- Estimated orthonormal coordinates of an ambient vector. -/
35 noncomputable def coordinates (V : OrthonormalBasis (Fin r) ℝ Q) :
36     E →L[ℝ] EuclideanSpace ℝ (Fin r) :=
37   V.repr.toContinuousLinearEquiv.toContinuousLinearMap.comp Q.orthogonalProjectionOnto
38 
39 /-- The column map of the true orthonormal basis. -/
40 noncomputable def synthesis (U : OrthonormalBasis (Fin r) ℝ P) :
41     EuclideanSpace ℝ (Fin r) →L[ℝ] E :=
42   P.subtypeL.comp U.repr.symm.toContinuousLinearEquiv.toContinuousLinearMap
43 
44 theorem coordinates_entry (V : OrthonormalBasis (Fin r) ℝ Q) (x : E) (i : Fin r) :
45     coordinates V x i = inner ℝ (V i:E) x := by
46   change V.repr (Q.orthogonalProjectionOnto x) i = _
47   rw [V.repr_apply_apply]
48   change inner ℝ (V i:E) (Q.starProjection x) = _
49   rw [← Q.inner_starProjection_left_eq_right,
50     Q.starProjection_eq_self_iff.mpr (V i).property]
51 
52 theorem cross_entry (U : OrthonormalBasis (Fin r) ℝ P)
53     (V : OrthonormalBasis (Fin r) ℝ Q) (i j : Fin r) :
54     cross U V i j = inner ℝ (V i:E) (U j:E) := by
55   simp only [cross, LinearMap.toMatrix_apply, OrthonormalBasis.coe_toBasis,
56     OrthonormalBasis.coe_toBasis_repr_apply]
57   exact coordinates_entry V (U j:E) i
58 
59 theorem cross_action (U : OrthonormalBasis (Fin r) ℝ P)
60     (V : OrthonormalBasis (Fin r) ℝ Q) (y : EuclideanSpace ℝ (Fin r)) :
61     (cross U V).toEuclideanLin y = V.repr (project P Q (U.repr.symm y)) :=
62   matrix_action U V (project P Q).toLinearMap y
63 
64 theorem cross_lower (U : OrthonormalBasis (Fin r) ℝ P)
65     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
66     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ)
67     (y : EuclideanSpace ℝ (Fin r)) :
68     Real.sqrt (1-δ^2)*‖y‖ ≤ ‖(cross U V).toEuclideanLin y‖ := by
69   rw [cross_action, V.repr.norm_map]
70   have h := coordinate_lower P Q δ hδ hsmall hgap (U.repr.symm y)
71   rwa [U.repr.symm.norm_map] at h
72 
73 /-- Actual smallest singular value of the square cross-basis matrix. -/
74 theorem cross_min_singular (U : OrthonormalBasis (Fin r) ℝ P)
75     (V : OrthonormalBasis (Fin r) ℝ Q) (hr : 0 < r) (δ : ℝ) (hδ : 0 ≤ δ)
76     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) :
77     Real.sqrt (1-δ^2) ≤ (cross U V).toEuclideanLin.singularValues (r-1) := by
78   have hd : Module.finrank ℝ (EuclideanSpace ℝ (Fin r)) = r := by simp
79   let i : Fin (Module.finrank ℝ (EuclideanSpace ℝ (Fin r))) := ⟨r-1, by omega⟩
80   have h := cross_lower U V δ hδ hsmall hgap (Spectral.rightBasis (cross U V).toEuclideanLin i)
81   rw [(Spectral.rightBasis (cross U V).toEuclideanLin).norm_eq_one, mul_one,
82     Spectral.image_basis_norm] at h
83   exact h
84 
85 omit [FiniteDimensional ℝ E] in
86 theorem basis_dimensions (U : OrthonormalBasis (Fin r) ℝ P)
87     (V : OrthonormalBasis (Fin r) ℝ Q) : Module.finrank ℝ P = Module.finrank ℝ Q :=
88   (Module.finrank_eq_card_basis U.toBasis).trans (Module.finrank_eq_card_basis V.toBasis).symm
89 
90 theorem coordinates_injective (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
91     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) :
92     Function.Injective ((coordinates V).comp P.subtypeL) := by
93   intro x y h
94   apply coordinate_injective P Q δ hδ hsmall hgap
95   exact V.repr.injective h
96 
97 end Komorebi.LSM.BasisCoordinates

Back to source controls