PolynomialParameterPath.lean

1 module
2 public import PolynomialPadicUnique
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 open Filter Topology
9 
10 namespace Komorebi.PolynomialParameterPath
11 open Komorebi.PolynomialPadicUnique
12 
13 variable {k : ℕ}
14 
15 /-- Truncate a prescribed p-adic parameter while retaining the exact initial
16 integer representative, rather than replacing it by its canonical residue. -/
17 def parameterPath (p L : ℕ) [Fact (Nat.Prime p)] (x : Fin k → ℤ)
18     (τ : Fin k → ℤ_[p]) : ℕ → Fin k → ℤ
19   | 0 => x
20   | n + 1 => truncInt p (L + n + 1) τ
21 
22 @[simp] theorem parameterPath_zero (p L : ℕ) [Fact (Nat.Prime p)]
23     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p]) :
24     parameterPath p L x τ 0 = x := rfl
25 
26 /-- Every stage retains its full requested precision relative to the target. -/
27 theorem parameterPath_precision (p L : ℕ) [Fact (Nat.Prime p)]
28     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p])
29     (hτ : ∀ i, (p : ℤ_[p])^L ∣ τ i - (x i : ℤ_[p])) (n : ℕ) (i : Fin k) :
30     (p : ℤ_[p])^(L+n) ∣ τ i - (parameterPath p L x τ n i : ℤ_[p]) := by
31   cases n with
32   | zero => simpa only [Nat.add_zero, parameterPath] using hτ i
33   | succ n =>
34       simpa only [parameterPath, Nat.add_assoc] using
35         truncInt_precision p (L+n+1) τ i
36 
37 /-- Successive parameter representatives are compatible over the integers. -/
38 theorem parameterPath_compatible (p L : ℕ) [Fact (Nat.Prime p)]
39     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p])
40     (hτ : ∀ i, (p : ℤ_[p])^L ∣ τ i - (x i : ℤ_[p])) :
41     ∀ n i, (p : ℤ)^(L+n) ∣
42       (parameterPath p L x τ (n+1) - parameterPath p L x τ n) i := by
43   intro n i
44   apply (int_pow_dvd_iff p (L+n) _).mpr
45   have hnext := dvd_trans (pow_dvd_pow (p : ℤ_[p]) (by omega : L+n ≤ L+(n+1)))
46     (parameterPath_precision p L x τ hτ (n+1) i)
47   simpa only [Pi.sub_apply, Int.cast_sub, sub_sub_sub_cancel_left] using
48     dvd_sub (parameterPath_precision p L x τ hτ n i) hnext
49 
50 /-- The constructed parameter path converges to the prescribed target itself. -/
51 theorem parameterPath_tendsto (p L : ℕ) [Fact (Nat.Prime p)]
52     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p])
53     (hτ : ∀ i, (p : ℤ_[p])^L ∣ τ i - (x i : ℤ_[p])) :
54     Tendsto (fun n i => (parameterPath p L x τ n i : ℤ_[p])) atTop (𝓝 τ) := by
55   apply tendsto_pi_nhds.mpr
56   intro i
57   rw [Metric.tendsto_atTop]
58   intro ε hε
59   obtain ⟨N, hN⟩ := PadicInt.exists_pow_neg_lt p hε
60   refine ⟨N, ?_⟩
61   intro n hn
62   have hd : (p : ℤ_[p])^N ∣ τ i - (parameterPath p L x τ n i : ℤ_[p]) :=
63     dvd_trans (pow_dvd_pow (p : ℤ_[p]) (by omega))
64       (parameterPath_precision p L x τ hτ n i)
65   have hb := (PadicInt.norm_le_pow_iff_mem_span_pow
66     (τ i - (parameterPath p L x τ n i : ℤ_[p])) N).mpr
67     (Ideal.mem_span_singleton.mpr hd)
68   rw [dist_comm, dist_eq_norm]
69   exact lt_of_le_of_lt hb hN
70 
71 /-- Every p-adic parameter in the base residue ball supplies an actual compatible
72 integer path, with exact initial representative and all retained precisions. -/
73 theorem exists_parameter_path (p L : ℕ) [Fact (Nat.Prime p)]
74     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p])
75     (hτ : ∀ i, (p : ℤ_[p])^L ∣ τ i - (x i : ℤ_[p])) :
76     ∃ t : ℕ → Fin k → ℤ,
77       t 0 = x ∧
78       (∀ n i, (p : ℤ)^(L+n) ∣ (t (n+1) - t n) i) ∧
79       (∀ n i, (p : ℤ_[p])^(L+n) ∣ τ i - (t n i : ℤ_[p])) ∧
80       Tendsto (fun n i => (t n i : ℤ_[p])) atTop (𝓝 τ) := by
81   exact ⟨parameterPath p L x τ, rfl,
82     parameterPath_compatible p L x τ hτ, parameterPath_precision p L x τ hτ,
83     parameterPath_tendsto p L x τ hτ⟩
84 
85 #print axioms parameterPath
86 #print axioms parameterPath_zero
87 #print axioms parameterPath_precision
88 #print axioms parameterPath_compatible
89 #print axioms parameterPath_tendsto
90 #print axioms exists_parameter_path
91 
92 end Komorebi.PolynomialParameterPath

Back to source controls