RationalLorentzAlgebra.lean

1 import KomorebiLSM.RationalLorentzMatrix
2 import KomorebiLSM.InteriorRepair
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.RationalLorentzMatrix
6 open scoped BigOperators
7 open LorentzCylinder RationalBernsteinMargin
8 noncomputable section
9 
10 theorem matrixOperator_qadd (M N : RationalMatrix) :
11     matrixOperator (qadd M N)=matrixOperator M+matrixOperator N := by
12   apply ContinuousLinearMap.ext
13   intro z
14   apply coordinate_ext
15   intro i
16   simp [coordinate_matrixOperator,qadd,add_mul,Finset.sum_add_distrib]
17 
18 theorem matrixOperator_qscale (q : ℚ) (M : RationalMatrix) :
19     matrixOperator (qscale q M)=(q : ℝ) • matrixOperator M := by
20   apply ContinuousLinearMap.ext
21   intro z
22   apply coordinate_ext
23   intro i
24   simp [coordinate_matrixOperator,qscale,Finset.mul_sum,mul_assoc]
25 
26 theorem matrixOperator_sub (M N : RationalMatrix) :
27     matrixOperator (M-N)=matrixOperator M-matrixOperator N := by
28   apply ContinuousLinearMap.ext
29   intro z
30   apply coordinate_ext
31   intro i
32   simp [coordinate_matrixOperator,sub_mul,Finset.sum_sub_distrib]
33 
34 @[simp] theorem matrixOperator_zero : matrixOperator (0 : RationalMatrix)=0 := by
35   apply ContinuousLinearMap.ext
36   intro z
37   apply coordinate_ext
38   intro i
39   simp [coordinate_matrixOperator]
40 
41 def centerMatrix : RationalMatrix := ![![1,0,0],![0,0,0],![0,0,0]]
42 
43 @[simp] theorem matrixOperator_center : matrixOperator centerMatrix=InteriorRepair.centerReset := by
44   apply ContinuousLinearMap.ext
45   intro z
46   apply coordinate_ext
47   intro i
48   simp only [coordinate_matrixOperator,InteriorRepair.centerReset_apply]
49   fin_cases i <;> norm_num [centerMatrix,coordinate,Fin.sum_univ_succ,Matrix.cons_val_two]
50 
51 end
52 end Komorebi.LSM.RationalLorentzMatrix

Back to source controls