PolynomialCoefficientPerturbation.lean

1 module
2 public import PolynomialPadicLift
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialCoefficientPerturbation
9 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
10 open Komorebi.PolynomialPadicLift Komorebi.PolynomialSurjectiveStep
11 variable {d e : ℕ}
12 
13 /-- An actual coefficient perturbation of an integer polynomial system. -/
14 def perturb (c : ℤ) (F H : Fin e → MvPolynomial (Fin d) ℤ) :
15     Fin e → MvPolynomial (Fin d) ℤ :=
16   fun i => F i + MvPolynomial.C c * H i
17 
18 /-- Integer evaluation of the perturbed system, derived from polynomial evaluation. -/
19 theorem evalSystem_perturb (c : ℤ) (F H : Fin e → MvPolynomial (Fin d) ℤ)
20     (x : Fin d → ℤ) (i : Fin e) :
21     evalSystem (perturb c F H) x i = evalSystem F x i + c * evalSystem H x i := by
22   simp [evalSystem, perturb]
23 
24 /-- Partial derivatives obey the same coefficient perturbation identity. -/
25 theorem pderiv_perturb (c : ℤ) (F H : Fin e → MvPolynomial (Fin d) ℤ)
26     (i : Fin e) (k : Fin d) :
27     MvPolynomial.pderiv k (perturb c F H i) =
28       MvPolynomial.pderiv k (F i) + MvPolynomial.C c * MvPolynomial.pderiv k (H i) := by
29   simp only [perturb, map_add, MvPolynomial.pderiv_C_mul]
30 
31 /-- A coefficient perturbation divisible by q preserves the actual reduced Jacobian. -/
32 theorem digitJacobian_perturb_eq (q : ℕ) (c : ℤ) (hc : (q : ℤ) ∣ c)
33     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
34     digitJacobian q (perturb c F H) x = digitJacobian q F x := by
35   have hc0 : (c : ZMod q) = 0 := (ZMod.intCast_zmod_eq_zero_iff_dvd c q).mpr hc
36   apply LinearMap.ext
37   intro t
38   ext i
39   change (∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (perturb c F H i)) : ZMod q) * t k) =
40     ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * t k
41   simp [pderiv_perturb, hc0]
42 
43 /-- Coefficient perturbations and movement inside one residue class preserve the same Jacobian. -/
44 theorem digitJacobian_perturb_point_eq (q : ℕ) (c : ℤ) (hc : (q : ℤ) ∣ c)
45     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x y : Fin d → ℤ)
46     (hxy : ∀ i, (q : ℤ) ∣ y i - x i) :
47     digitJacobian q (perturb c F H) y = digitJacobian q F x := by
48   rw [digitJacobian_perturb_eq q c hc F H y]
49   exact digitJacobian_eq q F x y hxy
50 
51 /-- A coefficient perturbation divisible by the prescribed precision preserves a lower root. -/
52 theorem lower_root_perturb (q L : ℕ) (c : ℤ) (hc : (q : ℤ)^L ∣ c)
53     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
54     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i) :
55     ∀ i, (q : ℤ)^L ∣ evalSystem (perturb c F H) x i := by
56   intro i
57   rw [evalSystem_perturb]
58   exact dvd_add (hx i) (dvd_mul_of_dvd_left hc _)
59 
60 /-- A positive-depth coefficient perturbation preserves smooth liftability and its initial precision. -/
61 theorem exists_padic_root_perturb (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
62     (c : ℤ) (hc : (p : ℤ)^L ∣ c)
63     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
64     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
65     (hJ : Function.Surjective (digitJacobian p F x)) :
66     ∃ a : Fin d → ℤ_[p],
67       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (perturb c F H i) = 0) ∧
68       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
69   have hpc : (p : ℤ) ∣ c :=
70     (dvd_pow_self (p : ℤ) (by omega : L ≠ 0)).trans hc
71   apply exists_padic_root p L hL (perturb c F H) x
72   · exact lower_root_perturb p L c hc F H x hx
73   · rw [digitJacobian_perturb_eq p c hpc F H x]
74     exact hJ
75 
76 /-- In particular, F + p^M H has a p-adic root at the original precision whenever M ≥ L ≥ 1. -/
77 theorem exists_padic_root_power_perturb (p L M : ℕ) [Fact (Nat.Prime p)]
78     (hL : 1 ≤ L) (hLM : L ≤ M)
79     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
80     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
81     (hJ : Function.Surjective (digitJacobian p F x)) :
82     ∃ a : Fin d → ℤ_[p],
83       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a
84         (F i + MvPolynomial.C ((p : ℤ)^M) * H i) = 0) ∧
85       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
86   exact exists_padic_root_perturb p L hL ((p : ℤ)^M)
87     (pow_dvd_pow (p : ℤ) hLM) F H x hx hJ
88 
89 /-- The p-adic evaluation identity uses the actual perturbed polynomial coefficients. -/
90 theorem padicEval_perturb (p : ℕ) [Fact (Nat.Prime p)]
91     (c : ℤ) (F H : Fin e → MvPolynomial (Fin d) ℤ)
92     (a : Fin d → ℤ_[p]) (i : Fin e) :
93     padicEval p (perturb c F H) a i = padicEval p F a i + (c : ℤ_[p]) * padicEval p H a i := by
94   simp only [padicEval, perturb, MvPolynomial.eval₂_add, MvPolynomial.eval₂_mul,
95     MvPolynomial.eval₂_C]
96   rfl
97 
98 end Komorebi.PolynomialCoefficientPerturbation

Back to source controls