PolynomialRootStabilityContract.lean

1 module
2 public import PolynomialRootStability
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialRootStabilityContract
8 
9 /-- A rectangular system has a nearby perturbed root whenever its actual
10 reduced Jacobian is surjective. Full coefficient precision M is retained. -/
11 theorem explicit_rectangular_nearby_root (p M : ℕ) [Fact (Nat.Prime p)]
12     (hM : 1 ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c) {d e : ℕ}
13     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
14     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin e =>
15       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k))
16     (a : Fin d → ℤ_[p])
17     (ha : ∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0)
18     (hax : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p])) :
19     ∃ b : Fin d → ℤ_[p],
20       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) b
21         (F i + MvPolynomial.C c * H i) = 0) ∧
22       (∀ i, (p : ℤ_[p])^M ∣ b i - a i) := by
23   exact PolynomialRootStability.exists_nearby_perturbed_root p M hM c hc F H x hJ a ha hax
24 
25 /-- The displacement bound applies to every perturbed root in the original
26 square residue ball, without choosing an auxiliary root as an assumption. -/
27 theorem explicit_square_root_displacement (p L M : ℕ) [Fact (Nat.Prime p)]
28     (hL : 1 ≤ L) (hLM : L ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c) {d : ℕ}
29     (F H : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
30     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin d =>
31       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k))
32     (a b : Fin d → ℤ_[p])
33     (ha : ∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0)
34     (hb : ∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) b
35       (F i + MvPolynomial.C c * H i) = 0)
36     (hax : ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p]))
37     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) :
38     ∀ i, (p : ℤ_[p])^M ∣ b i - a i := by
39   exact PolynomialRootStability.perturbed_roots_congruent p L M hL hLM c hc F H x hJ
40     a b ha hb hax hbx
41 
42 /-- From one lower root, obtain the original exact root and a unique exact
43 perturbed root. The Jacobian is evaluated from F, not supplied as an unrelated matrix. -/
44 theorem explicit_lower_root_and_unique_perturbation (p L M : ℕ) [Fact (Nat.Prime p)]
45     (hL : 1 ≤ L) (hLM : L ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c) {d : ℕ}
46     (F H : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
47     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i))
48     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin d =>
49       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k)) :
50     ∃ a : Fin d → ℤ_[p],
51       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
52       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) ∧
53       ∃! b : Fin d → ℤ_[p],
54         (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) b
55           (F i + MvPolynomial.C c * H i) = 0) ∧
56         (∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) ∧
57         (∀ i, (p : ℤ_[p])^M ∣ b i - a i) := by
58   exact PolynomialRootStability.exists_root_and_unique_perturbation
59     p L M hL hLM c hc F H x hx hJ
60 
61 end Komorebi.PolynomialRootStabilityContract

Back to source controls