PolynomialWeightedLiftContract.lean

1 module
2 public import PolynomialWeightedLift
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialWeightedLiftContract
8 open MvPolynomial
9 variable {d : ℕ}
10 
11 /-- An expanded contract using the actual evaluated derivative matrix and an
12 integral inverse certificate; no normalization or contraction is a hypothesis. -/
13 theorem actual_jacobian_integral_certificate (p s r : ℕ) [Fact p.Prime]
14     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
15     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
16     (hAJ : A * (Matrix.of fun i j => eval a (pderiv j (F i))) =
17       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
18     (hJA : (Matrix.of fun i j => eval a (pderiv j (F i))) * A =
19       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
20     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
21     ∃ b : Fin d → ℤ_[p],
22       (∀ i, eval b (F i) = 0) ∧
23       (∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) ∧
24       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
25       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (F i) = 0) →
26         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) :=
27   PolynomialWeightedLift.exists_weighted_root_certificate p s r hr F a A hAJ hJA hF
28 
29 /-- The written rational inverse hypothesis is applied to the actual Jacobian.
30 Uniqueness is on the entire stated ball and the root has the sharper depth r-s. -/
31 theorem actual_jacobian_bounded_inverse (p s r : ℕ) [Fact p.Prime]
32     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
33     (a : Fin d → ℤ_[p])
34     (hJ : IsUnit ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
35       (fun i j => eval a (pderiv j (F i)))))
36     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
37       (algebraMap ℤ_[p] ℚ_[p]).mapMatrix A = (p : ℚ_[p]) ^ s •
38         ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix (fun i j => eval a (pderiv j (F i))))⁻¹)
39     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
40     (∃! b : Fin d → ℤ_[p], (∀ i, eval b (F i) = 0) ∧
41       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i)) ∧
42     (∀ b : Fin d → ℤ_[p], (∀ i, eval b (F i) = 0) →
43       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) →
44       ∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) :=
45   PolynomialWeightedLift.exists_unique_weighted_root p s r hr F a hJ hbound hF
46 
47 end Komorebi.PolynomialWeightedLiftContract

Back to source controls