PolynomialMotionEstimate.lean

1 module
2 public import PolynomialTaylorDisplacement
3 public import PolynomialWeightedInverse
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialMotionEstimate
10 open scoped BigOperators
11 open MvPolynomial PolynomialWeightedInverse
12 variable {d : ℕ}
13 
14 /-- First-order displacement with the original Jacobian inverse certificate.
15 This estimate applies to any actual perturbed root having the weighted root bound. -/
16 theorem first_order_error_dvd (p s M : ℕ) [Fact p.Prime]
17     (F H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (a b : Fin d → ℤ_[p])
18     (A : Matrix (Fin d) (Fin d) ℤ_[p]) (hM : 2 * s < M)
19     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s •
20       (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
21     (hFa : ∀ i, eval a (F i) = 0)
22     (hRoot : ∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0)
23     (hDepth : ∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) :
24     ∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣
25       b i - a i + (p : ℤ_[p]) ^ (M - s) *
26         (A.mulVec (fun j => eval a (H j))) i := by
27   have hFa' (i : Fin d) : eval a (precondition A F i) = 0 := by
28     simp [precondition, hFa]
29   have hRoot' (i : Fin d) : eval b (precondition A F i) +
30       (p : ℤ_[p]) ^ M * eval b (precondition A H i) = 0 := by
31     simp only [precondition, map_sum, map_mul, eval_C]
32     rw [Finset.mul_sum, ← Finset.sum_add_distrib]
33     apply Finset.sum_eq_zero
34     intro j _
35     calc
36       A i j * eval b (F j) + (p : ℤ_[p]) ^ M * (A i j * eval b (H j)) =
37           A i j * (eval b (F j) + (p : ℤ_[p]) ^ M * eval b (H j)) := by ring
38       _ = 0 := by rw [hRoot j, mul_zero]
39   have hlin (i : Fin d) :
40       (∑ j, eval a (pderiv j (precondition A F i)) * (b j - a j)) =
41         (p : ℤ_[p]) ^ s * (b i - a i) := by
42     change (jacobian (precondition A F) a).mulVec (fun j => b j - a j) i = _
43     rw [jacobian_precondition, hAJ, Matrix.smul_mulVec, Matrix.one_mulVec]
44     rfl
45   have hp : (p : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
46   have hsM : s ≤ M := by omega
47   have hpowM : (p : ℤ_[p]) ^ M = (p : ℤ_[p]) ^ s * (p : ℤ_[p]) ^ (M - s) := by
48     rw [← pow_add, Nat.add_sub_of_le hsM]
49   have hexp : s + (2 * M - 3 * s) = (M - s) * 2 := by omega
50   have hpow : (p : ℤ_[p]) ^ s * (p : ℤ_[p]) ^ (2 * M - 3 * s) =
51       ((p : ℤ_[p]) ^ (M - s)) ^ 2 := by
52     rw [← pow_add, hexp, pow_mul]
53   intro i
54   have hTaylor := PolynomialTaylorDisplacement.taylor_remainder_dvd
55     (precondition A F i) a b ((p : ℤ_[p]) ^ (M - s)) hDepth
56   rw [hFa' i, sub_zero, hlin i] at hTaylor
57   have hVariation := PolynomialTaylorRing.eval_dvd_of_dvd
58     (precondition A H i) a b ((p : ℤ_[p]) ^ (M - s)) hDepth
59   have hVariationM : ((p : ℤ_[p]) ^ (M - s)) ^ 2 ∣
60       (p : ℤ_[p]) ^ M * (eval b (precondition A H i) - eval a (precondition A H i)) := by
61     rw [pow_two]
62     exact mul_dvd_mul (pow_dvd_pow (p : ℤ_[p]) (by omega)) hVariation
63   have hBig : ((p : ℤ_[p]) ^ (M - s)) ^ 2 ∣
64       (p : ℤ_[p]) ^ s * (b i - a i) + (p : ℤ_[p]) ^ M * eval a (precondition A H i) := by
65     convert dvd_neg.mpr (dvd_add hTaylor hVariationM) using 1
66     linear_combination hRoot' i
67   rw [congrFun (eval_precondition A H a) i] at hBig
68   apply (mul_dvd_mul_iff_left (pow_ne_zero s hp)).mp
69   rw [hpow, mul_add, ← mul_assoc, ← hpowM]
70   exact hBig
71 
72 end Komorebi.PolynomialMotionEstimate

Back to source controls