RationalTransform.lean

1 import KomorebiLSM.RationalBernsteinTermination
2 import Mathlib.Topology.Instances.Matrix
3 import Mathlib.Topology.Instances.Rat
4 
5 set_option autoImplicit false
6 namespace Komorebi.LSM.RationalTransform
7 open scoped BigOperators Matrix
8 open LorentzCylinder
9 noncomputable section
10 
11 abbrev RealMatrix := Matrix (Fin 3) (Fin 3) ℝ
12 abbrev RationalMatrix := Matrix (Fin 3) (Fin 3) ℚ
13 abbrev Vector := Fin 3 → ℝ
14 abbrev Parameters (R : Type*) := Fin 2 → Fin 3 → R
15 
16 /-- Literal mass, real and imaginary coordinates. -/
17 def coordinates : State ℂ ≃ₗ[ℝ] Vector where
18   toFun z := ![z.1,z.2.re,z.2.im]
19   invFun v := (v 0,⟨v 1,v 2⟩)
20   left_inv z := by rfl
21   right_inv v := by funext i; fin_cases i <;> rfl
22   map_add' x y := by funext i; fin_cases i <;> rfl
23   map_smul' a x := by funext i; fin_cases i <;> simp [Complex.real_smul]
24 
25 /-- A matrix acts through the actual fixed coordinate equivalence. -/
26 def operatorLinear : RealMatrix →ₗ[ℝ] (State ℂ →L[ℝ] State ℂ) where
27   toFun M := coordinates.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp
28     ((M.mulVecLin.toContinuousLinearMap).comp coordinates.toContinuousLinearEquiv.toContinuousLinearMap)
29   map_add' M N := by
30     apply ContinuousLinearMap.ext
31     intro z
32     apply coordinates.injective
33     simp
34   map_smul' a M := by
35     apply ContinuousLinearMap.ext
36     intro z
37     apply coordinates.injective
38     simp
39 
40 def operator (M : RealMatrix) : State ℂ →L[ℝ] State ℂ := operatorLinear M
41 
42 @[simp] theorem coordinates_operator (M : RealMatrix) (z : State ℂ) :
43     coordinates (operator M z) = M *ᵥ coordinates z := by
44   change coordinates (coordinates.symm (M *ᵥ coordinates z)) = _
45   exact coordinates.apply_symm_apply _
46 
47 theorem operator_mul (M N : RealMatrix) : operator (M*N) = (operator M).comp (operator N) := by
48   apply ContinuousLinearMap.ext
49   intro z
50   apply coordinates.injective
51   simp only [coordinates_operator, ContinuousLinearMap.comp_apply]
52   rw [Matrix.mulVec_mulVec]
53 
54 @[simp] theorem operator_one : operator (1 : RealMatrix) = ContinuousLinearMap.id ℝ (State ℂ) := by
55   apply ContinuousLinearMap.ext
56   intro z
57   apply coordinates.injective
58   simp
59 
60 theorem continuous_operator : Continuous (operator : RealMatrix → (State ℂ →L[ℝ] State ℂ)) :=
61   operatorLinear.continuous_of_finiteDimensional
62 
63 /-- The P75 rational operator is exactly the real matrix action. -/
64 def castMatrix (M : RationalMatrix) : RealMatrix := M.map (algebraMap ℚ ℝ)
65 
66 theorem operator_castMatrix (M : RationalMatrix) :
67     operator (castMatrix M) = RationalBernsteinMargin.matrixOperator M := by
68   apply ContinuousLinearMap.ext
69   intro z
70   apply coordinates.injective
71   funext i
72   change (coordinates (operator (castMatrix M) z)) i = _
73   rw [coordinates_operator]
74   have h := RationalBernsteinMargin.coordinate_matrixOperator M i z
75   convert h using 1 <;> fin_cases i <;> rfl
76 
77 /-- Invertibility is actual nonsingular matrix invertibility. -/
78 def atlas (M : RealMatrix) (hM : IsUnit M.det) : State ℂ ≃ₗ[ℝ] State ℂ where
79   toFun := operator M
80   invFun := operator M⁻¹
81   left_inv z := by
82     have h := congrArg (fun F : State ℂ →L[ℝ] State ℂ => F z)
83       (operator_mul M⁻¹ M)
84     rw [Matrix.nonsing_inv_mul _ hM, operator_one] at h
85     exact h.symm
86   right_inv z := by
87     have h := congrArg (fun F : State ℂ →L[ℝ] State ℂ => F z)
88       (operator_mul M M⁻¹)
89     rw [Matrix.mul_nonsing_inv _ hM, operator_one] at h
90     exact h.symm
91   map_add' := (operator M).map_add
92   map_smul' := (operator M).map_smul
93 
94 /-- The first row is fixed exactly, with all six remaining entries free. -/
95 def MassPreserving {R : Type*} [Zero R] [One R] (M : Matrix (Fin 3) (Fin 3) R) : Prop :=
96   M 0 = ![1,0,0]
97 
98 theorem mass_preserving_operator (M : RealMatrix) (hM : MassPreserving M) (z : State ℂ) :
99     (operator M z).1 = z.1 := by
100   have h := congrArg (fun v : Vector => v 0) (coordinates_operator M z)
101   change (operator M z).1 = _ at h
102   rw [Matrix.mulVec, dotProduct, hM] at h
103   simp [Fin.sum_univ_three] at h
104   exact h
105 
106 /-- Parameterizing the affine mass-row space preserves its constraint exactly. -/
107 def affineMatrix {R : Type*} [Zero R] [One R] (p : Parameters R) : Matrix (Fin 3) (Fin 3) R :=
108   ![![1,0,0],p 0,p 1]
109 
110 @[simp] theorem affineMatrix_mass {R : Type*} [Zero R] [One R] (p : Parameters R) :
111     MassPreserving (affineMatrix p) := rfl
112 
113 def parametersOf (M : RealMatrix) : Parameters ℝ := ![M 1,M 2]
114 
115 theorem affineMatrix_parametersOf (M : RealMatrix) (hM : MassPreserving M) :
116     affineMatrix (parametersOf M) = M := by
117   funext i
118   fin_cases i
119   · exact hM.symm
120   · rfl
121   · rfl
122 
123 def castParameters (p : Parameters ℚ) : Parameters ℝ := fun i j => (p i j : ℝ)
124 
125 theorem affineMatrix_cast (p : Parameters ℚ) :
126     affineMatrix (castParameters p) = castMatrix (affineMatrix p) := by
127   ext i j
128   change (affineMatrix (castParameters p)) i j = ((affineMatrix p) i j : ℝ)
129   fin_cases i <;> fin_cases j <;> simp [affineMatrix,castParameters]
130 
131 theorem continuous_affineMatrix : Continuous (affineMatrix (R := ℝ)) := by
132   apply continuous_pi
133   intro i
134   fin_cases i
135   · exact continuous_const
136   · exact continuous_apply 0
137   · exact continuous_apply 1
138 
139 theorem dense_castParameters : DenseRange castParameters := by
140   exact DenseRange.piMap (fun _ : Fin 2 => DenseRange.piMap (fun _ : Fin 3 => Rat.denseRange_cast))
141 
142 @[simp] theorem castMatrix_one : castMatrix (1 : RationalMatrix) = 1 := by
143   simp [castMatrix]
144 
145 @[simp] theorem castMatrix_mul (M N : RationalMatrix) : castMatrix (M*N) = castMatrix M*castMatrix N := by
146   simp [castMatrix, Matrix.map_mul]
147 
148 @[simp] theorem det_castMatrix (M : RationalMatrix) : (castMatrix M).det = (M.det : ℝ) :=
149   ((algebraMap ℚ ℝ).map_det M).symm
150 
151 theorem unit_castMatrix (M : RationalMatrix) (hM : IsUnit M.det) : IsUnit (castMatrix M).det := by
152   rw [isUnit_iff_ne_zero,det_castMatrix]
153   exact_mod_cast (isUnit_iff_ne_zero.mp hM)
154 
155 theorem unit_of_castMatrix (M : RationalMatrix) (hM : IsUnit (castMatrix M).det) : IsUnit M.det := by
156   rw [isUnit_iff_ne_zero] at hM ⊢
157   rw [det_castMatrix] at hM
158   exact_mod_cast hM
159 
160 /-- Rational inversion and real inversion are the same actual inverse. -/
161 theorem castMatrix_inv (M : RationalMatrix) (hM : IsUnit M.det) :
162     castMatrix M⁻¹ = (castMatrix M)⁻¹ := by
163   have hr := unit_castMatrix M hM
164   have he : castMatrix M * castMatrix M⁻¹ = 1 := by
165     rw [← castMatrix_mul, Matrix.mul_nonsing_inv _ hM, castMatrix_one]
166   calc
167     castMatrix M⁻¹ = (castMatrix M)⁻¹ * (castMatrix M * castMatrix M⁻¹) := by
168       rw [← Matrix.mul_assoc,Matrix.nonsing_inv_mul _ hr,Matrix.one_mul]
169     _ = (castMatrix M)⁻¹ := by rw [he,Matrix.mul_one]
170 
171 /-- Forward similarity is the literal submitted coordinate transformation. -/
172 def conjugate (T : RealMatrix) (F : State ℂ →L[ℝ] State ℂ) : State ℂ →L[ℝ] State ℂ :=
173   (operator T).comp (F.comp (operator T⁻¹))
174 
175 variable {n : ℕ}
176 def conjugated (T : RealMatrix) (G : Fin n → RationalMatrix) (u : ℝ) : State ℂ →L[ℝ] State ℂ :=
177   conjugate T (PolynomialGram.operatorPolynomial (fun k => operator (castMatrix (G k))) u)
178 
179 def rationalConjugated (T : RationalMatrix) (G : Fin n → RationalMatrix) : Fin n → RationalMatrix :=
180   fun k => T*G k*T⁻¹
181 
182 theorem conjugated_polynomial (T : RealMatrix) (G : Fin n → RationalMatrix) (u : ℝ) :
183     conjugated T G u = PolynomialGram.operatorPolynomial
184       (fun k => conjugate T (operator (castMatrix (G k)))) u := by
185   apply ContinuousLinearMap.ext
186   intro z
187   simp [conjugated,conjugate,PolynomialGram.operatorPolynomial,sum_apply,smul_apply]
188 
189 /-- The rational transformed coefficients give exactly the full inverse-conjugated density. -/
190 theorem rational_conjugated_operator (T : RationalMatrix) (hT : IsUnit T.det)
191     (G : Fin n → RationalMatrix) (u : ℝ) :
192     PolynomialGram.operatorPolynomial (fun k => RationalBernsteinMargin.matrixOperator (rationalConjugated T G k)) u =
193       conjugated (castMatrix T) G u := by
194   rw [conjugated_polynomial]
195   congr 1
196   funext k
197   rw [← operator_castMatrix]
198   simp only [rationalConjugated,castMatrix_mul,castMatrix_inv T hT,operator_mul]
199   rfl
200 
201 theorem continuousAt_inverse (T : RealMatrix) (hT : IsUnit T.det) :
202     ContinuousAt (Inv.inv : RealMatrix → RealMatrix) T := by
203   apply continuousAt_matrix_inv T
204   rw [Ring.inverse_eq_inv']
205   exact continuousAt_inv₀ (isUnit_iff_ne_zero.mp hT)
206 
207 theorem continuous_slack : Continuous (RobustOrientedMargin.slack : State ℂ → ℝ) :=
208   continuous_fst.sub continuous_snd.norm
209 
210 /-- Continuity is derived under the actual matrix inverse at an invertible transform. -/
211 theorem continuousAt_conjugated (G : Fin n → RationalMatrix) (T : RealMatrix)
212     (hT : IsUnit T.det) (u : ℝ) :
213     ContinuousAt (fun Tu : RealMatrix×ℝ => conjugated Tu.1 G Tu.2) (T,u) := by
214   have hleft : ContinuousAt (fun Tu : RealMatrix×ℝ => operator Tu.1) (T,u) :=
215     continuous_operator.continuousAt.comp continuous_fst.continuousAt
216   have hright : ContinuousAt (fun Tu : RealMatrix×ℝ => operator Tu.1⁻¹) (T,u) :=
217     continuous_operator.continuousAt.comp ((continuousAt_inverse T hT).comp continuous_fst.continuousAt)
218   have hmiddle : ContinuousAt (fun Tu : RealMatrix×ℝ =>
219       PolynomialGram.operatorPolynomial (fun k => operator (castMatrix (G k))) Tu.2) (T,u) :=
220     (PolynomialGram.operatorPolynomial_continuous _).continuousAt.comp continuous_snd.continuousAt
221   exact hleft.clm_comp (hmiddle.clm_comp hright)
222 
223 /-- Rational initial coordinates have the same literal state interpretation. -/
224 def rationalState (z : Fin 3 → ℚ) : State ℂ :=
225   ((z 0 : ℝ),⟨(z 1 : ℝ),(z 2 : ℝ)⟩)
226 
227 @[simp] theorem coordinates_rationalState (z : Fin 3 → ℚ) :
228     coordinates (rationalState z) = fun i => (z i : ℝ) := by
229   funext i
230   fin_cases i <;> rfl
231 
232 theorem operator_rationalState (M : RationalMatrix) (z : Fin 3 → ℚ) :
233     operator (castMatrix M) (rationalState z) = rationalState (M *ᵥ z) := by
234   apply coordinates.injective
235   rw [coordinates_operator]
236   simp only [coordinates_rationalState]
237   funext i
238   exact ((algebraMap ℚ ℝ).map_mulVec M z i).symm
239 
240 /-- A finite rational strict-cone test has no square root. -/
241 def StrictVector (z : Fin 3 → ℚ) : Prop :=
242   0<z 0 ∧ z 1^2+z 2^2<z 0^2
243 
244 theorem strictVector_iff_slack (z : Fin 3 → ℚ) :
245     StrictVector z ↔ 0<RobustOrientedMargin.slack (rationalState z) := by
246   have hs : ‖(rationalState z).2‖^2 = (z 1 : ℝ)^2+(z 2 : ℝ)^2 := by
247     rw [← Complex.normSq_eq_norm_sq]
248     simp [rationalState,Complex.normSq_apply,pow_two]
249   constructor
250   · rintro ⟨hm,hq⟩
251     have hmR : 0<(z 0 : ℝ) := by exact_mod_cast hm
252     have hqR : (z 1 : ℝ)^2+(z 2 : ℝ)^2<(z 0 : ℝ)^2 := by exact_mod_cast hq
253     change 0<(z 0 : ℝ)-‖(rationalState z).2‖
254     nlinarith [norm_nonneg (rationalState z).2]
255   · intro h
256     change 0<(z 0 : ℝ)-‖(rationalState z).2‖ at h
257     have hmR : 0<(z 0 : ℝ) := by linarith [norm_nonneg (rationalState z).2]
258     have hqR : (z 1 : ℝ)^2+(z 2 : ℝ)^2<(z 0 : ℝ)^2 := by
259       nlinarith [norm_nonneg (rationalState z).2]
260     exact ⟨by exact_mod_cast hmR,by exact_mod_cast hqR⟩
261 
262 theorem mass_preserving_inverse (M : RealMatrix) (hM : IsUnit M.det)
263     (hmass : MassPreserving M) (z : State ℂ) : (operator M⁻¹ z).1=z.1 := by
264   have he : operator M (operator M⁻¹ z)=z := (atlas M hM).apply_symm_apply z
265   have h := mass_preserving_operator M hmass (operator M⁻¹ z)
266   rw [he] at h
267   exact h.symm
268 
269 theorem conjugate_weighted (T : RealMatrix) (F : Fin n → State ℂ →L[ℝ] State ℂ)
270     (w : Fin n → ℝ) :
271     conjugate T (∑ k,w k • F k) = ∑ k,w k • conjugate T (F k) := by
272   apply ContinuousLinearMap.ext
273   intro z
274   simp [conjugate,sum_apply,smul_apply]
275 
276 /-- Exact averaged mass transports through the actual inverse, independently of cone positivity. -/
277 theorem conjugate_mass (T : RealMatrix) (hT : IsUnit T.det) (hmass : MassPreserving T)
278     (F : Fin n → State ℂ →L[ℝ] State ℂ) (w : Fin n → ℝ)
279     (hF : ∀ z, ((∑ k,w k • F k) z).1=z.1) (z : State ℂ) :
280     ((∑ k,w k • conjugate T (F k)) z).1=z.1 := by
281   rw [← conjugate_weighted]
282   change (operator T ((∑ k,w k • F k) (operator T⁻¹ z))).1=z.1
283   rw [mass_preserving_operator T hmass, hF, mass_preserving_inverse T hT hmass]
284 
285 theorem rational_conjugated_coefficient (T : RationalMatrix) (hT : IsUnit T.det)
286     (G : Fin n → RationalMatrix) (k : Fin n) :
287     RationalBernsteinMargin.matrixOperator (rationalConjugated T G k) =
288       conjugate (castMatrix T) (operator (castMatrix (G k))) := by
289   rw [← operator_castMatrix]
290   simp only [rationalConjugated,castMatrix_mul,castMatrix_inv T hT,operator_mul]
291   rfl
292 
293 end
294 end Komorebi.LSM.RationalTransform

Back to source controls