DecoderMatrixFormula.lean

1 import KomorebiLSM.BasisDecoder
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.BasisCoordinates
5 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
6 variable [FiniteDimensional ℝ E] {m r : ℕ} {P Q : Submodule ℝ E}
7 
8 /-- Columns of a subspace basis in an ambient orthonormal basis. -/
9 noncomputable def columns (W : OrthonormalBasis (Fin m) ℝ E)
10     (U : OrthonormalBasis (Fin r) ℝ P) : Matrix (Fin m) (Fin r) ℝ :=
11   LinearMap.toMatrix U.toBasis W.toBasis P.subtype
12 
13 omit [FiniteDimensional ℝ E] in
14 theorem columns_entry (W : OrthonormalBasis (Fin m) ℝ E)
15     (U : OrthonormalBasis (Fin r) ℝ P) (i : Fin m) (j : Fin r) :
16     columns W U i j = inner ℝ (W i) (U j:E) := by
17   simp [columns, LinearMap.toMatrix_apply, W.repr_apply_apply]
18 
19 theorem cross_eq_transpose_mul (W : OrthonormalBasis (Fin m) ℝ E)
20     (U : OrthonormalBasis (Fin r) ℝ P) (V : OrthonormalBasis (Fin r) ℝ Q) :
21     cross U V = (columns W V).transpose * columns W U := by
22   ext i j
23   rw [cross_entry, Matrix.mul_apply]
24   simp only [Matrix.transpose_apply, columns_entry]
25   simpa only [real_inner_comm (V i:E)] using
26     (W.sum_inner_mul_inner (V i:E) (U j:E)).symm
27 
28 omit [FiniteDimensional ℝ E] in
29 theorem columns_action (W : OrthonormalBasis (Fin m) ℝ E)
30     (U : OrthonormalBasis (Fin r) ℝ P) (y : EuclideanSpace ℝ (Fin r)) :
31     (columns W U).toEuclideanLin y = W.repr (synthesis U y) :=
32   matrix_action U W P.subtype y
33 
34 /-- Literal ambient matrix formula for the decoder, with the ordinary matrix inverse. -/
35 theorem decoder_matrix_formula (W : OrthonormalBasis (Fin m) ℝ E)
36     (U : OrthonormalBasis (Fin r) ℝ P) (V : OrthonormalBasis (Fin r) ℝ Q)
37     (y : EuclideanSpace ℝ (Fin r)) :
38     W.repr (decoder U V y) =
39       (columns W U * ((columns W V).transpose * columns W U)⁻¹).toEuclideanLin y := by
40   rw [← cross_eq_transpose_mul W U V]
41   change W.repr (synthesis U ((cross U V)⁻¹.toEuclideanLin y)) = _
42   rw [← columns_action]
43   exact (congrArg (fun T : EuclideanSpace ℝ (Fin r) →ₗ[ℝ] EuclideanSpace ℝ (Fin m) => T y)
44     (Matrix.toLpLin_mul_same 2 (columns W U) (cross U V)⁻¹)).symm
45 
46 end Komorebi.LSM.BasisCoordinates

Back to source controls