RationalLorentzMatrix.lean

1 import KomorebiLSM.RationalBernsteinMargin
2 import Mathlib.Algebra.MvPolynomial.Funext
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.RationalLorentzMatrix
6 open scoped BigOperators
7 open LorentzCylinder RationalBernsteinMargin TensorBernsteinCertificate
8 noncomputable section
9 
10 theorem coordinate_ext {z w : State ℂ} (h : ∀ i,coordinate i z=coordinate i w) : z=w := by
11   apply Prod.ext
12   · simpa [coordinate] using h 0
13   · apply Complex.ext
14     · simpa [coordinate] using h 1
15     · simpa [coordinate] using h 2
16 
17 def qadd (M N : RationalMatrix) : RationalMatrix := fun i j => M i j+N i j
18 
19 def qscale (q : ℚ) (M : RationalMatrix) : RationalMatrix := fun i j => q*M i j
20 
21 def qmul (M N : RationalMatrix) : RationalMatrix := fun i j => ∑ k,M i k*N k j
22 
23 theorem matrixOperator_qmul (M N : RationalMatrix) :
24     matrixOperator (qmul M N)=(matrixOperator M).comp (matrixOperator N) := by
25   apply ContinuousLinearMap.ext
26   intro z
27   apply coordinate_ext
28   intro i
29   simp only [coordinate_matrixOperator,ContinuousLinearMap.comp_apply,qmul,
30     Rat.cast_sum,Rat.cast_mul,Finset.sum_mul,Finset.mul_sum]
31   rw [Finset.sum_comm]
32   apply Finset.sum_congr rfl
33   intro j _
34   apply Finset.sum_congr rfl
35   intro k _
36   ring
37 
38 theorem matrixOperator_add (M N : RationalMatrix) :
39     matrixOperator (M+N)=matrixOperator M+matrixOperator N := by
40   apply ContinuousLinearMap.ext
41   intro z
42   apply coordinate_ext
43   intro i
44   simp [coordinate_matrixOperator,add_mul,Finset.sum_add_distrib]
45 
46 theorem matrixOperator_smul (q : ℚ) (M : RationalMatrix) :
47     matrixOperator (q • M)=(q : ℝ) • matrixOperator M := by
48   apply ContinuousLinearMap.ext
49   intro z
50   apply coordinate_ext
51   intro i
52   simp [coordinate_matrixOperator,Finset.mul_sum,mul_assoc]
53 
54 theorem matrixOperator_mul (M N : RationalMatrix) :
55     matrixOperator (M*N)=(matrixOperator M).comp (matrixOperator N) := by
56   apply ContinuousLinearMap.ext
57   intro z
58   apply coordinate_ext
59   intro i
60   simp only [coordinate_matrixOperator,ContinuousLinearMap.comp_apply,Matrix.mul_apply,
61     Rat.cast_sum,Rat.cast_mul,Finset.sum_mul,Finset.mul_sum]
62   rw [Finset.sum_comm]
63   apply Finset.sum_congr rfl
64   intro j _
65   apply Finset.sum_congr rfl
66   intro k _
67   ring
68 
69 theorem matrixOperator_one : matrixOperator (1 : RationalMatrix)=ContinuousLinearMap.id ℝ (State ℂ) := by
70   apply ContinuousLinearMap.ext
71   intro z
72   apply coordinate_ext
73   intro i
74   simp only [coordinate_matrixOperator,Matrix.one_apply,apply_ite]
75   simp
76 
77 /-- Equality of the finite rational polynomials can be proved through exact real identities. -/
78 theorem polynomial_eq_of_value_eq (p q : Polynomial₂) (h : ∀ x,value p x=value q x) : p=q := by
79   apply MvPolynomial.map_injective (algebraMap ℚ ℝ) (FaithfulSMul.algebraMap_injective ℚ ℝ)
80   apply MvPolynomial.funext
81   intro x
82   simpa only [value,MvPolynomial.eval_map] using h x
83 
84 end
85 end Komorebi.LSM.RationalLorentzMatrix

Back to source controls