CoordinateBasisChange.lean

1 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
2 import Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
3 import Mathlib.Tactic
4 
5 /-!
6 # Coordinate changes for a normal-equation covector
7 
8 These finite matrix identities are the basis-change part of WR15. The index
9 types may be empty. No orthonormality assumption is made on the change matrix.
10 The Hilbert-space interpretation and invertibility of a basis Gram matrix are
11 established in `CoordinateCovector`.
12 -/
13 
14 set_option autoImplicit false
15 
16 open Matrix
17 
18 namespace KomorebiSpace.CoordinateCovector
19 
20 variable {m n k : Type*} [Fintype m] [Fintype n]
21 
22 /-- The residual of the coordinate normal equation, regarded as a covector. -/
23 def normalResidual (S : Matrix m n ℝ) (G : Matrix n n ℝ)
24     (α : ℝ) (c : n → ℝ) (r : m → ℝ) : n → ℝ :=
25   (Sᵀ * S + α • G) *ᵥ c - Sᵀ *ᵥ r
26 
27 /-- The Gram matrix transforms by congruence, for every finite change matrix. -/
28 theorem gram_matrix_basis_change (B : Matrix m n ℝ) (C : Matrix n n ℝ) :
29     (B * C)ᵀ * (B * C) = Cᵀ * (Bᵀ * B) * C := by
30   simp only [Matrix.transpose_mul, Matrix.mul_assoc]
31 
32 /-- The matrix of the observed correction transforms with the same change matrix. -/
33 theorem observation_matrix_basis_change
34     (d : Matrix k m ℝ) (B : Matrix m n ℝ) (C : Matrix n n ℝ) :
35     d * (B * C) = (d * B) * C := by
36   rw [Matrix.mul_assoc]
37 
38 /-- A transpose moves between the two factors of the real dot product. -/
39 theorem transpose_mulVec_dotProduct (C : Matrix m n ℝ)
40     (q : m → ℝ) (v : n → ℝ) :
41     dotProduct (Cᵀ *ᵥ q) v = dotProduct q (C *ᵥ v) := by
42   classical
43   simp only [Matrix.mulVec, dotProduct, Matrix.transpose_apply]
44   simp_rw [Finset.sum_mul, Finset.mul_sum]
45   rw [Finset.sum_comm]
46   apply Finset.sum_congr rfl
47   intro i hi
48   apply Finset.sum_congr rfl
49   intro j hj
50   ring
51 
52 variable [DecidableEq n]
53 
54 /-- Applying an invertible change and its inverse preserves a coefficient vector. -/
55 theorem change_mul_inverse_mulVec (C : Matrix n n ℝ) (hC : IsUnit C)
56     (c : n → ℝ) : C *ᵥ (C⁻¹ *ᵥ c) = c := by
57   rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv C
58     (C.isUnit_iff_isUnit_det.mp hC), Matrix.one_mulVec]
59 
60 omit [Fintype m] in
61 /-- The changed coordinates represent exactly the same ambient correction. -/
62 theorem correction_basis_change (B : Matrix m n ℝ) (C : Matrix n n ℝ)
63     (hC : IsUnit C) (c : n → ℝ) :
64     (B * C) *ᵥ (C⁻¹ *ᵥ c) = B *ᵥ c := by
65   rw [← Matrix.mulVec_mulVec, change_mul_inverse_mulVec C hC]
66 
67 omit [Fintype m] in
68 /-- For independent columns, preservation of the correction forces the inverse
69 coordinate transformation. -/
70 theorem coordinates_basis_change (B : Matrix m n ℝ)
71     (hB : Function.Injective B.mulVec) (C : Matrix n n ℝ)
72     (hC : IsUnit C) (c c' : n → ℝ) :
73     (B * C) *ᵥ c' = B *ᵥ c ↔ c' = C⁻¹ *ᵥ c := by
74   constructor
75   · intro h
76     have hc : C *ᵥ c' = c := hB (by simpa only [Matrix.mulVec_mulVec] using h)
77     have hi := congrArg (fun v => C⁻¹ *ᵥ v) hc
78     simpa only [Matrix.mulVec_mulVec, Matrix.nonsing_inv_mul C
79       (C.isUnit_iff_isUnit_det.mp hC), Matrix.one_mulVec] using hi
80   · intro h
81     rw [h, correction_basis_change B C hC]
82 
83 /-- Covariance is derived from the changed coordinate normal equation. -/
84 theorem normalResidual_basis_change (S : Matrix m n ℝ) (G : Matrix n n ℝ)
85     (C : Matrix n n ℝ) (hC : IsUnit C) (α : ℝ)
86     (c : n → ℝ) (r : m → ℝ) :
87     normalResidual (S * C) (Cᵀ * G * C) α (C⁻¹ *ᵥ c) r =
88       Cᵀ *ᵥ normalResidual S G α c r := by
89   simp only [normalResidual, Matrix.transpose_mul, Matrix.add_mulVec,
90     Matrix.smul_mulVec, ← Matrix.mulVec_mulVec, Matrix.mulVec_sub,
91     Matrix.mulVec_add, Matrix.mulVec_smul, change_mul_inverse_mulVec C hC]
92 
93 /-- The inverse metric transforms in the reverse order. This identity even
94 holds for the total matrix inverse when the metric is singular. -/
95 theorem inverse_gram_basis_change (G C : Matrix n n ℝ) :
96     (Cᵀ * G * C)⁻¹ = C⁻¹ * G⁻¹ * (C⁻¹)ᵀ := by
97   simp only [Matrix.mul_inv_rev, ← Matrix.transpose_nonsing_inv, Matrix.mul_assoc]
98 
99 /-- The inverse-Gram quadratic form is unchanged by any invertible coordinate
100 change; the covector transforms by the transpose. -/
101 theorem inverse_gram_quadratic_basis_change (G C : Matrix n n ℝ)
102     (hC : IsUnit C) (q : n → ℝ) :
103     dotProduct (Cᵀ *ᵥ q) ((Cᵀ * G * C)⁻¹ *ᵥ (Cᵀ *ᵥ q)) =
104       dotProduct q (G⁻¹ *ᵥ q) := by
105   have hCC : C * C⁻¹ = 1 :=
106     Matrix.mul_nonsing_inv C (C.isUnit_iff_isUnit_det.mp hC)
107   have hCT : (C⁻¹)ᵀ * Cᵀ = 1 := by
108     rw [← Matrix.transpose_mul, hCC, Matrix.transpose_one]
109   rw [inverse_gram_basis_change, transpose_mulVec_dotProduct]
110   simp only [← Matrix.mulVec_mulVec]
111   rw [Matrix.mulVec_mulVec q (C⁻¹)ᵀ Cᵀ, hCT, Matrix.one_mulVec,
112     change_mul_inverse_mulVec C hC]
113 
114 /-- The certificate computed from the changed equation has the same value. -/
115 theorem normalResidual_certificate_basis_change
116     (S : Matrix m n ℝ) (G C : Matrix n n ℝ) (hC : IsUnit C)
117     (α : ℝ) (c : n → ℝ) (r : m → ℝ) :
118     let q' := normalResidual (S * C) (Cᵀ * G * C) α (C⁻¹ *ᵥ c) r
119     dotProduct q' ((Cᵀ * G * C)⁻¹ *ᵥ q') =
120       dotProduct (normalResidual S G α c r) (G⁻¹ *ᵥ normalResidual S G α c r) := by
121   dsimp only
122   rw [normalResidual_basis_change S G C hC]
123   exact inverse_gram_quadratic_basis_change G C hC _
124 
125 /-- Empty coefficient spaces produce the zero scalar certificate. -/
126 theorem zero_dimensional_certificate (G : Matrix (Fin 0) (Fin 0) ℝ)
127     (q : Fin 0 → ℝ) : dotProduct q (G⁻¹ *ᵥ q) = 0 := by
128   simp [dotProduct]
129 
130 section FullBasis
131 
132 open Module
133 
134 variable {H : Type*} [AddCommGroup H] [Module ℝ H]
135 
136 /-- Every invertible coordinate matrix determines a basis of the same entire
137 space, with its columns transformed by that matrix. -/
138 noncomputable def changedBasis (B : Basis n ℝ H) (C : Matrix n n ℝ)
139     (hC : IsUnit C) : Basis n ℝ H :=
140   B.map (Matrix.toLinearEquiv B C (C.isUnit_iff_isUnit_det.mp hC))
141 
142 /-- The changed basis columns are exactly `B C`. -/
143 theorem changedBasis_apply (B : Basis n ℝ H) (C : Matrix n n ℝ)
144     (hC : IsUnit C) (j : n) :
145     changedBasis B C hC j = B.equivFun.symm (fun i => C i j) := by
146   simp only [changedBasis, Basis.map_apply, Matrix.toLinearEquiv_apply,
147     Matrix.toLin_self, Basis.equivFun_symm_apply]
148 
149 /-- Synthesis in the changed full basis is synthesis after matrix transport. -/
150 theorem changedBasis_synthesis (B : Basis n ℝ H) (C : Matrix n n ℝ)
151     (hC : IsUnit C) (c : n → ℝ) :
152     (changedBasis B C hC).equivFun.symm c = B.equivFun.symm (C *ᵥ c) := by
153   rw [changedBasis, Basis.map_equivFun]
154   change Matrix.toLin B B C (B.equivFun.symm c) = B.equivFun.symm (C *ᵥ c)
155   rw [Matrix.toLin_apply, ← B.equivFun_apply,
156     LinearEquiv.apply_symm_apply, Basis.equivFun_symm_apply]
157 
158 /-- The inverse coordinates synthesize the same vector in the changed basis. -/
159 theorem changedBasis_same_vector (B : Basis n ℝ H) (C : Matrix n n ℝ)
160     (hC : IsUnit C) (c : n → ℝ) :
161     (changedBasis B C hC).equivFun.symm (C⁻¹ *ᵥ c) = B.equivFun.symm c := by
162   rw [changedBasis_synthesis, change_mul_inverse_mulVec C hC]
163 
164 /-- Coordinates of a fixed vector transform by the inverse matrix. -/
165 theorem changedBasis_coordinates (B : Basis n ℝ H) (C : Matrix n n ℝ)
166     (hC : IsUnit C) (x : H) :
167     (changedBasis B C hC).equivFun x = C⁻¹ *ᵥ B.equivFun x := by
168   apply (changedBasis B C hC).equivFun.symm.injective
169   rw [LinearEquiv.symm_apply_apply, changedBasis_same_vector,
170     LinearEquiv.symm_apply_apply]
171 
172 end FullBasis
173 
174 end KomorebiSpace.CoordinateCovector

Back to source controls