PolynomialPadicLiftContract.lean

1 module
2 public import PolynomialPadicLift
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open Filter Topology
8 namespace Komorebi.PolynomialPadicLiftContract
9 
10 /-- The root theorem with original polynomial evaluation and the full formal
11 Jacobian formula expanded. There is exactly one initial surjectivity hypothesis. -/
12 theorem explicit_padic_root (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
13     {d e : ℕ} (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
14     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i))
15     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin e =>
16       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k)) :
17     ∃ a : Fin d → ℤ_[p],
18       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
19       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
20   exact PolynomialPadicLift.exists_padic_root p L hL F x hx hJ
21 
22 /-- The same initial data give an actual convergent sequence, every retained
23 precision, the exact root, the fixed reduced Jacobian, and all finite lift counts. -/
24 theorem explicit_padic_root_with_tower (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
25     {d e : ℕ} (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
26     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i))
27     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin e =>
28       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k)) :
29     ∃ z : ℕ → Fin d → ℤ, ∃ a : Fin d → ℤ_[p],
30       z 0 = x ∧
31       (∀ n i, (p : ℤ)^(L+n) ∣ MvPolynomial.eval (z n) (F i)) ∧
32       (∀ n i, (p : ℤ)^(L+n) ∣ z (n+1) i - z n i) ∧
33       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a) ∧
34       (∀ n i, (p : ℤ_[p])^(L+n) ∣ a i - (z n i : ℤ_[p])) ∧
35       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
36       (∀ n, PolynomialDigitBridge.digitJacobian p F (z n) =
37         PolynomialDigitBridge.digitJacobian p F x) ∧
38       (∀ n, Nat.card (PolynomialLiftCounts.ActualLifts p (L+n) F (z n)) = p^(d-e)) := by
39   exact PolynomialPadicLift.exists_padic_root_with_tower p L hL F x hx hJ
40 
41 end Komorebi.PolynomialPadicLiftContract

Back to source controls