PolynomialMotionNormalization.lean

1 module
2 
3 public import PolynomialWeightedNormalization
4 
5 @[expose] public section
6 
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialMotionNormalization
11 
12 open scoped BigOperators
13 open MvPolynomial
14 open Komorebi.PolynomialTaylorRing Komorebi.PolynomialWeightedInverse
15 open Komorebi.PolynomialWeightedNormalization
16 
17 variable {d : ℕ}
18 
19 /-- The actual polynomial perturbation, including its specified power of the prime. -/
20 def perturbSystem (p M : ℕ) [Fact (Nat.Prime p)]
21     (F H : Fin d → MvPolynomial (Fin d) ℤ_[p]) :
22     Fin d → MvPolynomial (Fin d) ℤ_[p] :=
23   fun i => F i + C ((p : ℤ_[p]) ^ M) * H i
24 
25 /-- Evaluation retains exactly the requested perturbation. -/
26 theorem eval_perturbSystem (p M : ℕ) [Fact (Nat.Prime p)]
27     (F H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (z : Fin d → ℤ_[p]) (i : Fin d) :
28     eval z (perturbSystem p M F H i) =
29       eval z (F i) + (p : ℤ_[p]) ^ M * eval z (H i) := by
30   simp [perturbSystem]
31 
32 /-- Constant matrix preconditioning commutes with the actual perturbation. -/
33 theorem precondition_perturbSystem (p M : ℕ) [Fact (Nat.Prime p)]
34     (A : Matrix (Fin d) (Fin d) ℤ_[p])
35     (F H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (i : Fin d) :
36     precondition A (perturbSystem p M F H) i =
37       precondition A F i + C ((p : ℤ_[p]) ^ M) * precondition A H i := by
38   simp only [precondition, perturbSystem, mul_add, Finset.sum_add_distrib,
39     Finset.mul_sum]
40   congr 1
41   apply Finset.sum_congr rfl
42   intro j _
43   ring
44 
45 /-- Scaled polynomial differences have a polynomial quotient vanishing at zero. -/
46 theorem exists_eval_scaled_difference {R : Type*} [CommRing R]
47     (P : MvPolynomial (Fin d) R) (a : Fin d → R) (c : R) :
48     ∃ Q : MvPolynomial (Fin d) R,
49       (∀ u : Fin d → R, eval (fun i => a i + c * u i) P =
50         eval a P + c * eval u Q) ∧
51       eval (0 : Fin d → R) Q = 0 := by
52   obtain ⟨Q, hQ, hQ0⟩ := exists_eval_scaled_remainder P a c
53   refine ⟨linearPart P a + C c * Q, ?_, ?_⟩
54   · intro u
55     rw [hQ u]
56     simp only [map_add, map_mul, eval_C, eval_linearPart]
57     ring
58   · simp only [map_add, map_mul, eval_C, eval_zero_linearPart, hQ0, mul_zero, add_zero]
59 
60 /-- Normalization uses the original Jacobian certificate. No Jacobian assumption
61 on the perturbed system is needed. -/
62 theorem exists_motion_normalization (p s M : ℕ) [Fact (Nat.Prime p)]
63     (hr : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
64     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
65     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s •
66       (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
67     (hF : ∀ i, eval a (F i) = 0) :
68     ∃ C₀ : Fin d → ℤ_[p], ∃ Q : Fin d → MvPolynomial (Fin d) ℤ_[p],
69       (∀ i, (p : ℤ_[p]) ^ (M - (2 * s + 1)) ∣ C₀ i) ∧
70       (∀ i, eval (0 : Fin d → ℤ_[p]) (Q i) = 0) ∧
71       (∀ (u : Fin d → ℤ_[p]) i,
72         eval (fun j => a j + (p : ℤ_[p]) ^ (s + 1) * u j)
73           (precondition A (perturbSystem p M F H) i) =
74           (p : ℤ_[p]) ^ (2 * s + 1) *
75             (C₀ i + u i + (p : ℤ_[p]) * eval u (Q i))) := by
76   have hAF : ∀ i, eval a (precondition A F i) = 0 := by
77     intro i
78     simp [precondition, hF]
79   choose QF hQF hQF0 using fun i => exists_eval_scaled_remainder
80     (precondition A F i) a ((p : ℤ_[p]) ^ (s + 1))
81   choose QH hQH hQH0 using fun i => exists_eval_scaled_difference
82     (precondition A H i) a ((p : ℤ_[p]) ^ (s + 1))
83   refine ⟨fun i => (p : ℤ_[p]) ^ (M - (2 * s + 1)) *
84       eval a (precondition A H i),
85     fun i => QF i + C ((p : ℤ_[p]) ^ (M - (s + 1))) * QH i,
86     fun i => dvd_mul_right _ _, ?_, ?_⟩
87   · intro i
88     simp only [map_add, map_mul, eval_C, hQF0, hQH0, mul_zero, add_zero]
89   · intro u i
90     rw [precondition_perturbSystem]
91     simp only [map_add, map_mul, eval_C]
92     rw [hQF i u, hQH i u, hAF i, precondition_directional p s F a A hAJ]
93     have hpow₀ : (p : ℤ_[p]) ^ (2 * s + 1) *
94         (p : ℤ_[p]) ^ (M - (2 * s + 1)) = (p : ℤ_[p]) ^ M := by
95       rw [← pow_add, Nat.add_sub_of_le (by omega)]
96     have hpow₁ : (p : ℤ_[p]) ^ (s + 1) * (p : ℤ_[p]) ^ s =
97         (p : ℤ_[p]) ^ (2 * s + 1) := by
98       rw [← pow_add]
99       congr 1
100       omega
101     have hpow₂ : ((p : ℤ_[p]) ^ (s + 1)) ^ 2 =
102         (p : ℤ_[p]) ^ (2 * s + 1) * (p : ℤ_[p]) := by
103       rw [← pow_mul, ← pow_succ]
104       congr 1
105       omega
106     have hpow₃ : (p : ℤ_[p]) ^ (2 * s + 1) * (p : ℤ_[p]) *
107         (p : ℤ_[p]) ^ (M - (s + 1)) =
108         (p : ℤ_[p]) ^ M * (p : ℤ_[p]) ^ (s + 1) := by
109       rw [← pow_succ, ← pow_add, ← pow_add]
110       congr 1
111       omega
112     rw [hpow₂]
113     linear_combination -(eval a (precondition A H i)) * hpow₀ +
114       (u i) * hpow₁ - (eval u (QH i)) * hpow₃
115 
116 end Komorebi.PolynomialMotionNormalization

Back to source controls