PolynomialRootMotionContract.lean

1 module
2 public import PolynomialRootMotion
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialRootMotionContract
9 open MvPolynomial
10 variable {d : ℕ}
11 
12 /-- The original actual Jacobian certificate constructs a perturbed root and gives
13 its integral first-order error. All polynomial evaluations are written out. -/
14 theorem original_jacobian_integral_error (p s M : ℕ) [Fact p.Prime]
15     (hM : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
16     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
17     (hAJ : A * (Matrix.of fun i j => eval a (pderiv j (F i))) =
18       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
19     (hJA : (Matrix.of fun i j => eval a (pderiv j (F i))) * A =
20       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
21     (hFa : ∀ i, eval a (F i) = 0) :
22     ∃ b : Fin d → ℤ_[p],
23       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
24       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
25       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
26       (∀ z : Fin d → ℤ_[p],
27         (∀ i, eval z (F i) + (p : ℤ_[p]) ^ M * eval z (H i) = 0) →
28         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) ∧
29       (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣
30         b i - a i + (p : ℤ_[p]) ^ (M - s) * A.mulVec (fun j => eval a (H j)) i) := by
31   obtain ⟨b, hb, hdepth, hball, huniq⟩ :=
32     PolynomialRootMotion.exists_perturbed_root_certificate p s M hM F H a A hAJ hJA hFa
33   have hroot : ∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0 := by
34     simpa only [PolynomialMotionNormalization.eval_perturbSystem] using hb
35   refine ⟨b, hroot, hdepth, hball, ?_, ?_⟩
36   · intro z hz hzb
37     apply huniq z _ hzb
38     simpa only [PolynomialMotionNormalization.eval_perturbSystem] using hz
39   · exact PolynomialMotionEstimate.first_order_error_dvd p s M F H a b A
40       hM hAJ hFa hroot hdepth
41 
42 /-- The exact rational formula uses the actual original derivative matrix and the
43 actual perturbation. Full-ball unique existence comes before the extra precision,
44 so uniqueness is not restricted to roots already satisfying the error estimate. -/
45 theorem original_jacobian_rational_motion (p s M : ℕ) [Fact p.Prime]
46     (hM : 2 * s < M) (F H : Fin d → MvPolynomial (Fin d) ℤ_[p])
47     (a : Fin d → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
48     (hJ : IsUnit ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
49       (fun i j => eval a (pderiv j (F i)))))
50     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
51       (algebraMap ℤ_[p] ℚ_[p]).mapMatrix A = (p : ℚ_[p]) ^ s •
52         ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix (fun i j => eval a (pderiv j (F i))))⁻¹) :
53     (∃! b : Fin d → ℤ_[p],
54       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
55       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i)) ∧
56     (∀ b : Fin d → ℤ_[p],
57       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) →
58       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) →
59       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
60       (∃ ε : Fin d → ℤ_[p], (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣ ε i) ∧
61         ∀ i, (b i : ℚ_[p]) - (a i : ℚ_[p]) =
62           -(p : ℚ_[p]) ^ M *
63             (((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
64               (fun k j => eval a (pderiv j (F k))))⁻¹).mulVec
65               (fun j => (eval a (H j) : ℚ_[p])) i + (ε i : ℚ_[p]))) := by
66   have result := PolynomialRootMotion.exists_unique_root_motion p s M hM F H a hFa hJ hbound
67   unfold PolynomialWeightedInverse.rationalMatrix at result
68   unfold PolynomialWeightedInverse.jacobian at result
69   simpa only [PolynomialMotionNormalization.eval_perturbSystem] using result
70 
71 end Komorebi.PolynomialRootMotionContract

Back to source controls