PolynomialWeightedAuxiliaryContract.lean

1 module
2 public import PolynomialTaylorRing
3 public import PolynomialPadicContraction
4 public import PolynomialWeightedInverse
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 namespace Komorebi.PolynomialWeightedAuxiliaryContract
10 open MvPolynomial
11 variable {d : ℕ}
12 
13 /-- The remainder is a single actual polynomial, uniform over every input. -/
14 theorem uniform_polynomial_taylor {R : Type*} [CommRing R]
15     (P : MvPolynomial (Fin d) R) (a : Fin d → R) (c : R) :
16     ∃ Q : MvPolynomial (Fin d) R,
17       (∀ u : Fin d → R, eval (fun i => a i + c * u i) P =
18         eval a P + c * (∑ i, eval a (pderiv i P) * u i) + c ^ 2 * eval u Q) ∧
19       eval (0 : Fin d → R) Q = 0 :=
20   PolynomialTaylorRing.exists_eval_scaled_remainder P a c
21 
22 /-- Arbitrary integral p-adic coefficients require no assumed Lipschitz estimate. -/
23 theorem actual_polynomial_contraction (p : ℕ) [Fact p.Prime]
24     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c : Fin d → ℤ_[p]) :
25     ∃! u : Fin d → ℤ_[p],
26       (fun i => c i + (p : ℤ_[p]) * eval u (H i)) = u :=
27   PolynomialPadicContraction.exists_unique_fixedPoint p H c
28 
29 /-- The denominator exponent is preserved exactly in the integral translation. -/
30 theorem exact_inverse_denominator_certificate (p s : ℕ) [Fact p.Prime]
31     (J : Matrix (Fin d) (Fin d) ℤ_[p]) :
32     (IsUnit ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix J) ∧
33       ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
34         (algebraMap ℤ_[p] ℚ_[p]).mapMatrix A =
35           (p : ℚ_[p]) ^ s • ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix J)⁻¹) ↔
36     (∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
37       A * J = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]) ∧
38       J * A = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) :=
39   PolynomialWeightedInverse.bounded_inverse_iff_certificate p s J
40 
41 end Komorebi.PolynomialWeightedAuxiliaryContract

Back to source controls