PolynomialCoefficientPerturbationContract.lean

1 module
2 public import PolynomialCoefficientPerturbation
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialCoefficientPerturbationContract
8 
9 /-- This contract expands both the original polynomial perturbation and its
10 formal derivative. The reduced Jacobian is unchanged under coefficient perturbation. -/
11 theorem explicit_perturbed_jacobian (q : ℕ) (c : ℤ) (hc : (q : ℤ) ∣ c)
12     {d e : ℕ} (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
13     (t : Fin d → ZMod q) (i : Fin e) :
14     (∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k
15       (F i + MvPolynomial.C c * H i)) : ZMod q) * t k) =
16     ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * t k := by
17   have h := PolynomialCoefficientPerturbation.digitJacobian_perturb_eq q c hc F H x
18   exact congrFun (LinearMap.congr_fun h t) i
19 
20 /-- A perturbed exact root is derived from an approximate original root and
21 one actual surjective Jacobian, with the original residue precision retained. -/
22 theorem explicit_power_perturbation_root (p L M : ℕ) [Fact (Nat.Prime p)]
23     (hL : 1 ≤ L) (hLM : L ≤ M) {d e : ℕ}
24     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
25     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i))
26     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin e =>
27       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k)) :
28     ∃ a : Fin d → ℤ_[p],
29       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a
30         (F i + MvPolynomial.C ((p : ℤ)^M) * H i) = 0) ∧
31       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
32   exact PolynomialCoefficientPerturbation.exists_padic_root_power_perturb
33     p L M hL hLM F H x hx hJ
34 
35 end Komorebi.PolynomialCoefficientPerturbationContract

Back to source controls