PolynomialJointSystem.lean

1 module
2 public import PolynomialParameterSystem
3 public import PolynomialMotionNormalization
4 public import PolynomialBlockInverse
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialJointSystem
11 open MvPolynomial Matrix
12 open Komorebi.PolynomialParameterSystem
13 open Komorebi.PolynomialWeightedInverse
14 open Komorebi.PolynomialMotionNormalization
15 
16 variable {e k : ℕ}
17 
18 /-- The actual partial Jacobian in the solved coordinates, over the coefficient ring. -/
19 def solvedJacobian {R : Type*} [CommRing R]
20     (F : Fin e → MvPolynomial (Fin (e + k)) R) (a : Fin (e + k) → R) :
21     Matrix (Fin e) (Fin e) R :=
22   fun i j => eval a (pderiv (Fin.castAdd k j) (F i))
23 
24 /-- The actual partial Jacobian in the prescribed parameter coordinates. -/
25 def parameterJacobian {R : Type*} [CommRing R]
26     (F : Fin e → MvPolynomial (Fin (e + k)) R) (a : Fin (e + k) → R) :
27     Matrix (Fin e) (Fin k) R :=
28   fun i j => eval a (pderiv (Fin.natAdd e j) (F i))
29 
30 /-- Append equations fixing the parameters to the given base value. -/
31 def augmented {R : Type*} [CommRing R]
32     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R) :
33     Fin (e + k) → MvPolynomial (Fin (e + k)) R :=
34   join F (fun j => X (Fin.natAdd e j) - C (t₀ j))
35 
36 /-- Append the negative parameter displacement to the coefficient perturbation. -/
37 def augmentedPerturbation {R : Type*} [CommRing R]
38     (H : Fin e → MvPolynomial (Fin (e + k)) R) (v : Fin k → R) :
39     Fin (e + k) → MvPolynomial (Fin (e + k)) R :=
40   join H (fun j => -C (v j))
41 
42 @[simp] theorem augmented_solved {R : Type*} [CommRing R]
43     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R) (i : Fin e) :
44     augmented F t₀ (Fin.castAdd k i) = F i := by simp [augmented]
45 
46 @[simp] theorem augmented_free {R : Type*} [CommRing R]
47     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R) (j : Fin k) :
48     augmented F t₀ (Fin.natAdd e j) = X (Fin.natAdd e j) - C (t₀ j) := by
49   simp [augmented]
50 
51 @[simp] theorem augmentedPerturbation_solved {R : Type*} [CommRing R]
52     (H : Fin e → MvPolynomial (Fin (e + k)) R) (v : Fin k → R) (i : Fin e) :
53     augmentedPerturbation H v (Fin.castAdd k i) = H i := by
54   simp [augmentedPerturbation]
55 
56 @[simp] theorem augmentedPerturbation_free {R : Type*} [CommRing R]
57     (H : Fin e → MvPolynomial (Fin (e + k)) R) (v : Fin k → R) (j : Fin k) :
58     augmentedPerturbation H v (Fin.natAdd e j) = -C (v j) := by
59   simp [augmentedPerturbation]
60 
61 /-- Evaluation of the augmented system retains the original equations and exact parameters. -/
62 theorem eval_augmented {R : Type*} [CommRing R]
63     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
64     (z : Fin (e + k) → R) :
65     (fun i => eval z (augmented F t₀ i)) =
66       join (fun i => eval z (F i)) (freePart z - t₀) := by
67   ext i
68   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
69     simp [freePart]
70 
71 /-- Evaluation of the augmented perturbation has the sign needed for the prescribed shift. -/
72 theorem eval_augmentedPerturbation {R : Type*} [CommRing R]
73     (H : Fin e → MvPolynomial (Fin (e + k)) R) (v : Fin k → R)
74     (z : Fin (e + k) → R) :
75     (fun i => eval z (augmentedPerturbation H v i)) =
76       join (fun i => eval z (H i)) (-v) := by
77   ext i
78   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp
79 
80 /-- An original exact root is an exact root of the system fixing its original parameters. -/
81 theorem augmented_root {R : Type*} [CommRing R]
82     (F : Fin e → MvPolynomial (Fin (e + k)) R) (a : Fin (e + k) → R)
83     (hF : ∀ i, eval a (F i) = 0) :
84     ∀ i, eval a (augmented F (freePart a) i) = 0 := by
85   intro i
86   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp [hF, freePart]
87 
88 @[simp] theorem jacobian_augmented_solved_solved {R : Type*} [CommRing R]
89     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
90     (a : Fin (e + k) → R) (i j : Fin e) :
91     jacobian (augmented F t₀) a (Fin.castAdd k i) (Fin.castAdd k j) =
92       solvedJacobian F a i j := by simp [jacobian, solvedJacobian]
93 
94 @[simp] theorem jacobian_augmented_solved_free {R : Type*} [CommRing R]
95     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
96     (a : Fin (e + k) → R) (i : Fin e) (j : Fin k) :
97     jacobian (augmented F t₀) a (Fin.castAdd k i) (Fin.natAdd e j) =
98       parameterJacobian F a i j := by simp [jacobian, parameterJacobian]
99 
100 @[simp] theorem jacobian_augmented_free_solved {R : Type*} [CommRing R]
101     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
102     (a : Fin (e + k) → R) (i : Fin k) (j : Fin e) :
103     jacobian (augmented F t₀) a (Fin.natAdd e i) (Fin.castAdd k j) = 0 := by
104   have hne : Fin.natAdd e i ≠ Fin.castAdd k j := by
105     intro h
106     have hv := congrArg Fin.val h
107     simp only [Fin.val_natAdd, Fin.val_castAdd] at hv
108     omega
109   simp [jacobian, pderiv_X, hne]
110 
111 @[simp] theorem jacobian_augmented_free_free {R : Type*} [CommRing R]
112     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
113     (a : Fin (e + k) → R) (i j : Fin k) :
114     jacobian (augmented F t₀) a (Fin.natAdd e i) (Fin.natAdd e j) =
115       (1 : Matrix (Fin k) (Fin k) R) i j := by
116   by_cases hij : i = j <;>
117     simp [jacobian, pderiv_X, Matrix.one_apply, hij]
118 
119 /-- The derivative of the actual augmented polynomial is the triangular block matrix. -/
120 theorem jacobian_augmented {R : Type*} [CommRing R]
121     (F : Fin e → MvPolynomial (Fin (e + k)) R) (t₀ : Fin k → R)
122     (a : Fin (e + k) → R) :
123     jacobian (augmented F t₀) a =
124       Komorebi.PolynomialBlockInverse.upperBlock
125         (solvedJacobian F a) (parameterJacobian F a) 1 := by
126   ext i j
127   refine Fin.addCases (fun i => ?_) (fun i => ?_) i <;>
128     refine Fin.addCases (fun j => ?_) (fun j => ?_) j <;> simp
129 
130 /-- The augmented perturbed root equations are precisely the original perturbed equations
131 and the requested parameter equality. -/
132 theorem perturb_augmented_root_iff (p M : ℕ) [Fact (Nat.Prime p)]
133     (F H : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
134     (t₀ v : Fin k → ℤ_[p]) (b : Fin (e + k) → ℤ_[p]) :
135     (∀ i, eval b (perturbSystem p M (augmented F t₀) (augmentedPerturbation H v) i) = 0) ↔
136       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
137       freePart b = t₀ + (p : ℤ_[p]) ^ M • v := by
138   constructor
139   · intro h
140     constructor
141     · intro i
142       simpa only [eval_perturbSystem, augmented_solved, augmentedPerturbation_solved]
143         using h (Fin.castAdd k i)
144     · ext j
145       have hj := h (Fin.natAdd e j)
146       simp only [eval_perturbSystem, augmented_free, augmentedPerturbation_free,
147         map_sub, eval_X, eval_C, map_neg] at hj
148       change b (Fin.natAdd e j) = t₀ j + (p : ℤ_[p]) ^ M * v j
149       linear_combination hj
150   · rintro ⟨hF, ht⟩ i
151     refine Fin.addCases (fun j => ?_) (fun j => ?_) i
152     · simpa only [eval_perturbSystem, augmented_solved, augmentedPerturbation_solved]
153         using hF j
154     · have hj := congrFun ht j
155       change b (Fin.natAdd e j) = t₀ j + (p : ℤ_[p]) ^ M * v j at hj
156       simp only [eval_perturbSystem, augmented_free, augmentedPerturbation_free,
157         map_sub, eval_X, eval_C, map_neg, hj]
158       ring
159 
160 end Komorebi.PolynomialJointSystem

Back to source controls