PolynomialRootMotion.lean

1 module
2 public import PolynomialWeightedLift
3 public import PolynomialMotionNormalization
4 public import PolynomialMotionEstimate
5 public import PolynomialMotionRational
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialRootMotion
12 open MvPolynomial PolynomialWeightedInverse PolynomialPadicContraction
13 open PolynomialWeightedLift PolynomialMotionNormalization
14 variable {d : ℕ}
15 
16 /-- Polynomial normalization yields a root, its retained precision, and uniqueness
17 throughout the full ball. The injective preconditioner may come from a different
18 original system, which is essential when the coefficients have been perturbed. -/
19 theorem exists_root_from_original_preconditioner (p s r : ℕ) [Fact p.Prime]
20     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
21     (a : Fin d → ℤ_[p]) (A J : Matrix (Fin d) (Fin d) ℤ_[p])
22     (hJA : J * A = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
23     (C : Fin d → ℤ_[p]) (Q : Fin d → MvPolynomial (Fin d) ℤ_[p])
24     (hC : ∀ i, (p : ℤ_[p]) ^ (r - (2 * s + 1)) ∣ C i)
25     (hQ : ∀ i, eval (0 : Fin d → ℤ_[p]) (Q i) = 0)
26     (hnorm : ∀ u i, eval (shiftedPoint p s a u) (precondition A F i) =
27       (p : ℤ_[p]) ^ (2 * s + 1) * (C i + u i + (p : ℤ_[p]) * eval u (Q i))) :
28     ∃ b : Fin d → ℤ_[p],
29       (∀ i, eval b (F i) = 0) ∧
30       (∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) ∧
31       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
32       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (F i) = 0) →
33         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) := by
34   let H : Fin d → MvPolynomial (Fin d) ℤ_[p] := fun i => -Q i
35   let c : Fin d → ℤ_[p] := fun i => -C i
36   have hH : evalSystem p H 0 = 0 := by
37     funext i
38     change eval (0 : Fin d → ℤ_[p]) (-Q i) = 0
39     rw [map_neg, hQ i, neg_zero]
40   have hc : ∀ i, (p : ℤ_[p]) ^ (r - (2 * s + 1)) ∣ c i :=
41     fun i => dvd_neg.mpr (hC i)
42   obtain ⟨u, hu, huniq⟩ := exists_unique_fixedPoint p H c
43   have hprec := fixedPoint_divisible p (r - (2 * s + 1)) H c u hH hu hc
44   have hp : (p : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
45   have hroot_iff (w : Fin d → ℤ_[p]) :
46       (∀ i, eval (shiftedPoint p s a w) (F i) = 0) ↔ contractionMap p H c w = w := by
47     have hpre := precondition_root_iff p s A J hJA F (shiftedPoint p s a w)
48     constructor
49     · intro hw
50       have hg : (fun i => eval (shiftedPoint p s a w) (precondition A F i)) = 0 :=
51         hpre.mpr (funext hw)
52       funext i
53       have hi := congrFun hg i
54       rw [hnorm] at hi
55       have hz : C i + w i + (p : ℤ_[p]) * eval w (Q i) = 0 :=
56         (mul_eq_zero.mp hi).resolve_left (pow_ne_zero _ hp)
57       change -C i + (p : ℤ_[p]) * eval w (-Q i) = w i
58       rw [map_neg]
59       linear_combination -hz
60     · intro hw
61       apply funext_iff.mp (hpre.mp ?_)
62       funext i
63       rw [hnorm]
64       have hi := congrFun hw i
65       change -C i + (p : ℤ_[p]) * eval w (-Q i) = w i at hi
66       rw [map_neg] at hi
67       have hz : C i + w i + (p : ℤ_[p]) * eval w (Q i) = 0 := by
68         linear_combination -hi
69       simp only [hz, mul_zero, Pi.zero_apply]
70   refine ⟨shiftedPoint p s a u, (hroot_iff u).mpr hu, ?_, ?_, ?_⟩
71   · intro i
72     obtain ⟨v, hv⟩ := hprec i
73     refine ⟨v, ?_⟩
74     have he : s + 1 + (r - (2 * s + 1)) = r - s := by omega
75     simp only [shiftedPoint, add_sub_cancel_left]
76     rw [hv, ← mul_assoc, ← pow_add, he]
77   · intro i
78     exact ⟨u i, by simp [shiftedPoint]⟩
79   · intro z hz hball
80     choose w hw using hball
81     have hzw : z = shiftedPoint p s a w := by
82       funext i
83       have hi := hw i
84       change z i = a i + (p : ℤ_[p]) ^ (s + 1) * w i
85       linear_combination hi
86     rw [hzw] at hz ⊢
87     exact congrArg (shiftedPoint p s a) (huniq w ((hroot_iff w).mp hz))
88 
89 /-- The original Jacobian inverse certificate constructs the nearby root of the
90 actual perturbed polynomial system, without an assumption on its new Jacobian. -/
91 theorem exists_perturbed_root_certificate (p s M : ℕ) [Fact p.Prime]
92     (hM : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
93     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
94     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
95     (hJA : jacobian F a * A = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
96     (hFa : ∀ i, eval a (F i) = 0) :
97     ∃ b : Fin d → ℤ_[p],
98       (∀ i, eval b (perturbSystem p M F H i) = 0) ∧
99       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
100       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
101       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (perturbSystem p M F H i) = 0) →
102         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) := by
103   obtain ⟨C, Q, hC, hQ, hnorm⟩ :=
104     exists_motion_normalization p s M hM F H a A hAJ hFa
105   exact exists_root_from_original_preconditioner p s M hM (perturbSystem p M F H)
106     a A (jacobian F a) hJA C Q hC hQ hnorm
107 
108 /-- Weighted first-order root motion, including construction and full-ball uniqueness
109 of the perturbed root, under the original actual Jacobian's inverse bound. -/
110 theorem exists_root_motion (p s M : ℕ) [Fact p.Prime]
111     (hM : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
112     (a : Fin d → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
113     (hJ : IsUnit (rationalMatrix p (jacobian F a)))
114     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
115       rationalMatrix p A = (p : ℚ_[p]) ^ s • (rationalMatrix p (jacobian F a))⁻¹) :
116     ∃ b : Fin d → ℤ_[p],
117       (∀ i, eval b (perturbSystem p M F H i) = 0) ∧
118       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
119       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
120       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (perturbSystem p M F H i) = 0) →
121         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) ∧
122       (∃ ε : Fin d → ℤ_[p], (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣ ε i) ∧
123         ∀ i, (b i : ℚ_[p]) - (a i : ℚ_[p]) =
124           -(p : ℚ_[p]) ^ M * ((rationalMatrix p (jacobian F a))⁻¹).mulVec
125             (fun j => (eval a (H j) : ℚ_[p])) i + (ε i : ℚ_[p])) := by
126   obtain ⟨A, hA⟩ := hbound
127   obtain ⟨hAJ, hJA⟩ := certificate_of_integral_inverse p s (jacobian F a) A hJ hA
128   obtain ⟨b, hb, hdepth, hball, huniq⟩ :=
129     exists_perturbed_root_certificate p s M hM F H a A hAJ hJA hFa
130   have hroot : ∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0 := by
131     intro i
132     simpa only [eval_perturbSystem] using hb i
133   have herror := PolynomialMotionEstimate.first_order_error_dvd p s M F H a b A
134     hM hAJ hFa hroot hdepth
135   obtain ⟨ε, hε, hformula⟩ := PolynomialMotionRational.exists_rational_error
136     p s M (2 * M - 3 * s) (by omega) (jacobian F a) A hA a b
137     (fun j => eval a (H j)) herror
138   exact ⟨b, hb, hdepth, hball, huniq, ε, hε, hformula⟩
139 
140 /-- The unique-existence form keeps the full uniqueness ball separate from the
141 additional displacement and first-order precision conclusions. -/
142 theorem exists_unique_root_motion (p s M : ℕ) [Fact p.Prime]
143     (hM : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
144     (a : Fin d → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
145     (hJ : IsUnit (rationalMatrix p (jacobian F a)))
146     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
147       rationalMatrix p A = (p : ℚ_[p]) ^ s • (rationalMatrix p (jacobian F a))⁻¹) :
148     (∃! b : Fin d → ℤ_[p], (∀ i, eval b (perturbSystem p M F H i) = 0) ∧
149       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i)) ∧
150     (∀ b : Fin d → ℤ_[p], (∀ i, eval b (perturbSystem p M F H i) = 0) →
151       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) →
152       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
153       (∃ ε : Fin d → ℤ_[p], (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣ ε i) ∧
154         ∀ i, (b i : ℚ_[p]) - (a i : ℚ_[p]) =
155           -(p : ℚ_[p]) ^ M * ((rationalMatrix p (jacobian F a))⁻¹).mulVec
156             (fun j => (eval a (H j) : ℚ_[p])) i + (ε i : ℚ_[p]))) := by
157   obtain ⟨b, hb, hdepth, hball, huniq, herror⟩ := exists_root_motion p s M hM F H a hFa hJ hbound
158   constructor
159   · exact ⟨b, ⟨hb, hball⟩, fun z hz => huniq z hz.1 hz.2⟩
160   · intro z hz hzb
161     rw [huniq z hz hzb]
162     exact ⟨hdepth, herror⟩
163 
164 end Komorebi.PolynomialRootMotion

Back to source controls