BasisDecoder.lean

1 import KomorebiLSM.BasisCoordinates
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.BasisCoordinates
5 open Komorebi.LSM.SubspaceCoordinates
6 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
7 variable [FiniteDimensional ℝ E] {r : ℕ} {P Q : Submodule ℝ E}
8 
9 /-- The explicit formula `U (Uhatᵀ U)⁻¹`, as an operator on Euclidean coordinates. -/
10 noncomputable def decoder (U : OrthonormalBasis (Fin r) ℝ P)
11     (V : OrthonormalBasis (Fin r) ℝ Q) : EuclideanSpace ℝ (Fin r) →L[ℝ] E :=
12   (synthesis U).comp ((cross U V)⁻¹.toEuclideanLin.toContinuousLinearMap)
13 
14 theorem cross_inverse_matrix (U : OrthonormalBasis (Fin r) ℝ P)
15     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
16     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) :
17     (cross U V)⁻¹ = LinearMap.toMatrix V.toBasis U.toBasis
18       (coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm.toLinearMap := by
19   apply Matrix.inv_eq_left_inv
20   let e := coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)
21   change LinearMap.toMatrix V.toBasis U.toBasis e.symm.toLinearMap *
22     LinearMap.toMatrix U.toBasis V.toBasis e.toLinearMap = 1
23   rw [← LinearMap.toMatrix_comp U.toBasis V.toBasis U.toBasis]
24   have he : e.symm.toLinearMap.comp e.toLinearMap = LinearMap.id := by
25     apply LinearMap.ext
26     intro x
27     exact e.symm_apply_apply x
28   rw [he, LinearMap.toMatrix_id]
29 
30 theorem decoder_apply (U : OrthonormalBasis (Fin r) ℝ P)
31     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
32     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ)
33     (y : EuclideanSpace ℝ (Fin r)) :
34     decoder U V y =
35       ((coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm
36         (V.repr.symm y) : E) := by
37   change (U.repr.symm ((cross U V)⁻¹.toEuclideanLin y) : E) = _
38   rw [cross_inverse_matrix U V δ hδ hsmall hgap, matrix_action,
39     U.repr.symm_apply_apply]
40   rfl
41 
42 theorem decoder_coordinates (U : OrthonormalBasis (Fin r) ℝ P)
43     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
44     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) (x : P) :
45     decoder U V (coordinates V (x:E)) = (x:E) := by
46   rw [decoder_apply U V δ hδ hsmall hgap]
47   change ((coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm
48     (V.repr.symm (V.repr (project P Q x))) : E) = _
49   rw [V.repr.symm_apply_apply]
50   exact congrArg Subtype.val
51     ((coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm_apply_apply x)
52 
53 theorem coordinates_decoder (U : OrthonormalBasis (Fin r) ℝ P)
54     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
55     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ)
56     (y : EuclideanSpace ℝ (Fin r)) : coordinates V (decoder U V y) = y := by
57   rw [decoder_apply U V δ hδ hsmall hgap]
58   change V.repr (project P Q
59     ((coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm
60       (V.repr.symm y))) = y
61   have he := (coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).apply_symm_apply
62     (V.repr.symm y)
63   change project P Q _ = _ at he
64   rw [he, V.repr.apply_symm_apply]
65 
66 theorem decoder_mem_true (U : OrthonormalBasis (Fin r) ℝ P)
67     (V : OrthonormalBasis (Fin r) ℝ Q) (y : EuclideanSpace ℝ (Fin r)) :
68     decoder U V y ∈ P := (U.repr.symm ((cross U V)⁻¹.toEuclideanLin y)).property
69 
70 theorem decoder_norm_bound (U : OrthonormalBasis (Fin r) ℝ P)
71     (V : OrthonormalBasis (Fin r) ℝ Q) (δ : ℝ) (hδ : 0 ≤ δ)
72     (hsmall : δ < 1) (hgap : ‖P.starProjection-Q.starProjection‖ ≤ δ) :
73     ‖decoder U V‖ ≤ (Real.sqrt (1-δ^2))⁻¹ := by
74   apply ContinuousLinearMap.opNorm_le_bound _ (inv_nonneg.mpr (Real.sqrt_nonneg _))
75   intro y
76   rw [decoder_apply U V δ hδ hsmall hgap]
77   have h := (coordinateEquiv P Q δ hδ hsmall hgap (basis_dimensions U V)).symm.toContinuousLinearMap.le_opNorm
78     (V.repr.symm y)
79   exact h.trans (by
80     rw [V.repr.symm.norm_map]
81     exact mul_le_mul_of_nonneg_right
82       (coordinate_inverse_bound P Q δ hδ hsmall hgap (basis_dimensions U V)) (norm_nonneg y))
83 
84 end Komorebi.LSM.BasisCoordinates

Back to source controls