PolynomialLocalMapContract.lean

1 module
2 public import PolynomialLocalSurjective
3 public import PolynomialInverseCongruence
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 namespace Komorebi.PolynomialLocalMapContract
9 open MvPolynomial
10 variable {d e : ℕ}
11 
12 /-- Expanded actual derivative and evaluation contract for arbitrary p-adic output targets. -/
13 theorem arbitrary_padic_target (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
14     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
15     (hJ : Function.Surjective (fun u : Fin d → ZMod p => fun i =>
16       ∑ j, (eval x (pderiv j (F i)) : ZMod p) * u j))
17     (t : Fin e → ℤ_[p])
18     (ht : ∀ i, (p : ℤ_[p])^L ∣ t i - (eval x (F i) : ℤ_[p])) :
19     ∃ a : Fin d → ℤ_[p],
20       (∀ i, eval₂ (Int.castRingHom ℤ_[p]) a (F i) = t i) ∧
21       ∀ j, (p : ℤ_[p])^L ∣ a j - (x j : ℤ_[p]) := by
22   obtain ⟨a, ha, hax⟩ := PolynomialLocalSurjective.exists_padic_preimage p L hL F x hJ t ht
23   exact ⟨a, fun i => congrFun ha i, hax⟩
24 
25 /-- On one nonsingular square residue class every depth of precision is reflected. -/
26 theorem all_depths_reflected (p N : ℕ) [Fact (Nat.Prime p)]
27     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
28     (hJ : Function.Surjective (fun u : Fin d → ZMod p => fun i =>
29       ∑ j, (eval x (pderiv j (F i)) : ZMod p) * u j))
30     (a b : Fin d → ℤ_[p])
31     (ha : ∀ j, (p : ℤ_[p]) ∣ a j - (x j : ℤ_[p]))
32     (hb : ∀ j, (p : ℤ_[p]) ∣ b j - (x j : ℤ_[p])) :
33     (∀ i, (p : ℤ_[p])^N ∣
34       eval₂ (Int.castRingHom ℤ_[p]) a (F i) - eval₂ (Int.castRingHom ℤ_[p]) b (F i)) ↔
35     (∀ j, (p : ℤ_[p])^N ∣ a j - b j) :=
36   PolynomialInverseCongruence.padic_congruence_iff p N F x hJ a b ha hb
37 
38 end Komorebi.PolynomialLocalMapContract

Back to source controls