PolynomialPadicContraction.lean

1 module
2 
3 public import Mathlib.NumberTheory.Padics.PadicIntegers
4 public import Mathlib.Topology.MetricSpace.Contracting
5 public import Mathlib.Algebra.MvPolynomial.Basic
6 public import Mathlib.Tactic
7 
8 @[expose] public section
9 noncomputable section
10 set_option autoImplicit false
11 
12 namespace Komorebi.PolynomialPadicContraction
13 
14 open MvPolynomial
15 
16 variable {d e : ℕ}
17 
18 /-- Evaluation of an actual polynomial system with arbitrary integral p-adic coefficients. -/
19 def evalSystem (p : ℕ) [Fact p.Prime]
20     (H : Fin e → MvPolynomial (Fin d) ℤ_[p]) (u : Fin d → ℤ_[p]) : Fin e → ℤ_[p] :=
21   fun i => MvPolynomial.eval u (H i)
22 
23 /-- Polynomial evaluation over a commutative ring preserves every principal congruence. -/
24 theorem eval_dvd_of_dvd {R : Type*} [CommRing R]
25     (P : MvPolynomial (Fin d) R) (x y : Fin d → R) (a : R)
26     (h : ∀ i, a ∣ x i - y i) : a ∣ eval x P - eval y P := by
27   induction P using MvPolynomial.induction_on with
28   | C c => simp
29   | add P Q hP hQ =>
30     simp only [map_add]
31     convert dvd_add hP hQ using 2
32     ring
33   | mul_X P j hP =>
34     obtain ⟨r, hr⟩ := hP
35     obtain ⟨s, hs⟩ := h j
36     refine ⟨r * x j + eval y P * s, ?_⟩
37     simp only [map_mul, eval_X]
38     linear_combination x j * hr + eval y P * hs
39 
40 /-- A p-adic integral polynomial is nonexpanding for the supremum metric. -/
41 theorem eval_dist_le (p : ℕ) [Fact p.Prime]
42     (P : MvPolynomial (Fin d) ℤ_[p]) (x y : Fin d → ℤ_[p]) :
43     dist (eval x P) (eval y P) ≤ dist x y := by
44   rw [dist_eq_norm]
45   induction P using MvPolynomial.induction_on with
46   | C c => simp
47   | add P Q hP hQ =>
48     have heq : eval x (P + Q) - eval y (P + Q) =
49         (eval x P - eval y P) + (eval x Q - eval y Q) := by simp; ring
50     rw [heq]
51     exact (PadicInt.nonarchimedean _ _).trans (max_le hP hQ)
52   | mul_X P j hP =>
53     have heq : eval x (P * X j) - eval y (P * X j) =
54         (eval x P - eval y P) * x j + eval y P * (x j - y j) := by simp; ring
55     rw [heq]
56     apply (PadicInt.nonarchimedean _ _).trans
57     apply max_le
58     · rw [norm_mul]
59       exact (mul_le_mul_of_nonneg_left (PadicInt.norm_le_one _) (norm_nonneg _)).trans
60         (by simpa using hP)
61     · rw [norm_mul]
62       apply (mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)).trans
63       simpa only [one_mul, ← dist_eq_norm] using dist_le_pi_dist x y j
64 
65 /-- Actual polynomial systems with p-adic integral coefficients are 1-Lipschitz. -/
66 theorem lipschitz_evalSystem (p : ℕ) [Fact p.Prime]
67     (H : Fin e → MvPolynomial (Fin d) ℤ_[p]) : LipschitzWith 1 (evalSystem p H) := by
68   apply LipschitzWith.of_dist_le_mul
69   intro x y
70   simp only [NNReal.coe_one, one_mul]
71   exact (dist_pi_le_iff dist_nonneg).2 fun i => eval_dist_le p (H i) x y
72 
73 /-- The normalized integral fixed-point map. -/
74 def contractionMap (p : ℕ) [Fact p.Prime]
75     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c : Fin d → ℤ_[p])
76     (u : Fin d → ℤ_[p]) : Fin d → ℤ_[p] :=
77   fun i => c i + (p : ℤ_[p]) * evalSystem p H u i
78 
79 /-- The factor p makes every such actual polynomial map strictly contracting. -/
80 theorem contracting_contractionMap (p : ℕ) [Fact p.Prime]
81     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c : Fin d → ℤ_[p]) :
82     ContractingWith ‖(p : ℤ_[p])‖₊ (contractionMap p H c) := by
83   constructor
84   · exact_mod_cast (PadicInt.norm_lt_one_iff_dvd (p : ℤ_[p])).2 (dvd_refl _)
85   · apply LipschitzWith.of_dist_le_mul
86     intro x y
87     apply (dist_pi_le_iff (mul_nonneg (norm_nonneg _) dist_nonneg)).2
88     intro i
89     change dist (c i + (p : ℤ_[p]) * evalSystem p H x i)
90       (c i + (p : ℤ_[p]) * evalSystem p H y i) ≤ ‖(p : ℤ_[p])‖ * dist x y
91     rw [dist_eq_norm]
92     have heq : c i + (p : ℤ_[p]) * evalSystem p H x i -
93         (c i + (p : ℤ_[p]) * evalSystem p H y i) =
94         (p : ℤ_[p]) * (evalSystem p H x i - evalSystem p H y i) := by ring
95     rw [heq, norm_mul]
96     exact mul_le_mul_of_nonneg_left (eval_dist_le p (H i) x y)
97       (norm_nonneg (p : ℤ_[p]))
98 
99 /-- Existence and uniqueness of the normalized vector fixed point, without an assumed
100 Lipschitz or contraction hypothesis on the polynomial system. -/
101 theorem exists_unique_fixedPoint (p : ℕ) [Fact p.Prime]
102     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c : Fin d → ℤ_[p]) :
103     ∃! u : Fin d → ℤ_[p], contractionMap p H c u = u := by
104   let hf := contracting_contractionMap p H c
105   exact ⟨hf.fixedPoint _, hf.fixedPoint_isFixedPt, fun u hu => hf.fixedPoint_unique hu⟩
106 
107 /-- If the polynomial correction vanishes at zero, every precision of the constant
108 term is inherited by the fixed point. -/
109 theorem fixedPoint_divisible (p N : ℕ) [Fact p.Prime]
110     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c u : Fin d → ℤ_[p])
111     (hH : evalSystem p H 0 = 0) (hu : contractionMap p H c u = u)
112     (hc : ∀ i, (p : ℤ_[p]) ^ N ∣ c i) : ∀ i, (p : ℤ_[p]) ^ N ∣ u i := by
113   suffices h : ∀ n : ℕ, (∀ i, (p : ℤ_[p]) ^ n ∣ c i) →
114       ∀ i, (p : ℤ_[p]) ^ n ∣ u i from h N hc
115   intro n
116   induction n with
117   | zero => simp
118   | succ n ih =>
119     intro hcn
120     have hun : ∀ i, (p : ℤ_[p]) ^ n ∣ u i :=
121       ih (fun i => dvd_trans (pow_dvd_pow _ (Nat.le_succ n)) (hcn i))
122     intro i
123     have hHi : eval (0 : Fin d → ℤ_[p]) (H i) = 0 := congrFun hH i
124     have hHn : (p : ℤ_[p]) ^ n ∣ evalSystem p H u i := by
125       simpa only [evalSystem, hHi, sub_zero, Pi.zero_apply] using
126         eval_dvd_of_dvd (H i) u 0 ((p : ℤ_[p]) ^ n) (by simpa using hun)
127     have hm : (p : ℤ_[p]) ^ (n + 1) ∣ (p : ℤ_[p]) * evalSystem p H u i := by
128       rw [pow_succ']
129       exact mul_dvd_mul_left _ hHn
130     have hui : c i + (p : ℤ_[p]) * evalSystem p H u i = u i := congrFun hu i
131     rw [← hui]
132     exact dvd_add (hcn i) hm
133 
134 /-- The unique fixed point satisfies every given constant-term divisibility bound. -/
135 theorem exists_unique_fixedPoint_divisible (p N : ℕ) [Fact p.Prime]
136     (H : Fin d → MvPolynomial (Fin d) ℤ_[p]) (c : Fin d → ℤ_[p])
137     (hH : evalSystem p H 0 = 0) (hc : ∀ i, (p : ℤ_[p]) ^ N ∣ c i) :
138     ∃! u : Fin d → ℤ_[p], contractionMap p H c u = u ∧
139       ∀ i, (p : ℤ_[p]) ^ N ∣ u i := by
140   obtain ⟨u, hu, huniq⟩ := exists_unique_fixedPoint p H c
141   exact ⟨u, ⟨hu, fixedPoint_divisible p N H c u hH hu hc⟩,
142     fun v hv => huniq v hv.1⟩
143 
144 end Komorebi.PolynomialPadicContraction

Back to source controls