PadicTowerLimit.lean

1 module
2 public import Mathlib.NumberTheory.Padics.PadicIntegers
3 public import Mathlib.Topology.MetricSpace.Cauchy
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 open Filter Topology
10 
11 namespace Komorebi.PadicTowerLimit
12 
13 /-- Later integer approximations retain every earlier prescribed precision. -/
14 theorem tower_pair_dvd (p L : ℕ) (z : ℕ → ℤ)
15     (hstep : ∀ n, (p : ℤ) ^ (L + n) ∣ z (n + 1) - z n)
16     (n m : ℕ) (hnm : n ≤ m) :
17     (p : ℤ) ^ (L + n) ∣ z m - z n := by
18   induction m, hnm using Nat.le_induction with
19   | base => simp
20   | succ m hnm ih =>
21       have hs : (p : ℤ) ^ (L + n) ∣ z (m + 1) - z m :=
22         (pow_dvd_pow (p : ℤ) (Nat.add_le_add_left hnm L)).trans (hstep m)
23       have he : (z (m + 1) - z m) + (z m - z n) = z (m + 1) - z n := by ring
24       rw [← he]
25       exact dvd_add hs ih
26 
27 /-- Compatible integer approximations are Cauchy in the actual p-adic metric. -/
28 theorem compatible_int_tower_cauchy (p L : ℕ) [Fact p.Prime]
29     (z : ℕ → ℤ)
30     (hstep : ∀ n, (p : ℤ) ^ (L + n) ∣ z (n + 1) - z n) :
31     CauchySeq (fun n => (z n : ℤ_[p])) := by
32   rw [Metric.cauchySeq_iff]
33   intro ε hε
34   obtain ⟨N, hN⟩ := PadicInt.exists_pow_neg_lt p hε
35   refine ⟨N, ?_⟩
36   intro m hm n hn
37   have hm' := tower_pair_dvd p L z hstep N m hm
38   have hn' := tower_pair_dvd p L z hstep N n hn
39   have hd : (p : ℤ) ^ (L + N) ∣ z m - z n := by
40     have he : (z m - z N) - (z n - z N) = z m - z n := by ring
41     rw [← he]
42     exact dvd_sub hm' hn'
43   have hd' : (p : ℤ) ^ N ∣ z m - z n :=
44     (pow_dvd_pow (p : ℤ) (Nat.le_add_left N L)).trans hd
45   have hb := (PadicInt.norm_int_le_pow_iff_dvd (p := p)).2 hd'
46   rw [dist_eq_norm]
47   simpa only [Int.cast_sub] using lt_of_le_of_lt hb hN
48 
49 /-- A compatible integer tower has a p-adic limit retaining every finite residue. -/
50 theorem compatible_int_tower_limit (p L : ℕ) [Fact p.Prime]
51     (z : ℕ → ℤ)
52     (hstep : ∀ n, (p : ℤ) ^ (L + n) ∣ z (n + 1) - z n) :
53     ∃ a : ℤ_[p],
54       Tendsto (fun n => (z n : ℤ_[p])) atTop (𝓝 a) ∧
55       ∀ n, (p : ℤ_[p]) ^ (L + n) ∣ a - (z n : ℤ_[p]) := by
56   obtain ⟨a, ha⟩ := cauchySeq_tendsto_of_complete
57     (compatible_int_tower_cauchy p L z hstep)
58   refine ⟨a, ha, ?_⟩
59   intro n
60   rw [← Ideal.mem_span_singleton,
61     ← PadicInt.norm_le_pow_iff_mem_span_pow]
62   apply le_of_tendsto ((ha.sub tendsto_const_nhds).norm)
63   filter_upwards [eventually_ge_atTop n] with m hm
64   have hb := (PadicInt.norm_int_le_pow_iff_dvd (p := p)).2
65     (tower_pair_dvd p L z hstep n m hm)
66   simpa only [Int.cast_sub] using hb
67 
68 /-- The same limit construction applies coordinatewise, with convergence in the product topology. -/
69 theorem compatible_vector_tower_limit {ι : Type*} (p L : ℕ) [Fact p.Prime]
70     (z : ℕ → ι → ℤ)
71     (hstep : ∀ n i, (p : ℤ) ^ (L + n) ∣ z (n + 1) i - z n i) :
72     ∃ a : ι → ℤ_[p],
73       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a) ∧
74       ∀ n i, (p : ℤ_[p]) ^ (L + n) ∣ a i - (z n i : ℤ_[p]) := by
75   choose a ha using fun i => compatible_int_tower_limit p L (fun n => z n i)
76     (fun n => hstep n i)
77   exact ⟨a, tendsto_pi_nhds.2 (fun i => (ha i).1), fun n i => (ha i).2 n⟩
78 
79 /-- Diverging divisibility precision forces the actual p-adic value to tend to zero. -/
80 theorem divisible_int_tendsto_zero (p L : ℕ) [Fact p.Prime]
81     (z : ℕ → ℤ) (hz : ∀ n, (p : ℤ) ^ (L + n) ∣ z n) :
82     Tendsto (fun n => (z n : ℤ_[p])) atTop (𝓝 0) := by
83   rw [Metric.tendsto_atTop]
84   intro ε hε
85   obtain ⟨N, hN⟩ := PadicInt.exists_pow_neg_lt p hε
86   refine ⟨N, ?_⟩
87   intro n hn
88   have hd : (p : ℤ) ^ N ∣ z n :=
89     (pow_dvd_pow (p : ℤ) (hn.trans (Nat.le_add_left n L))).trans (hz n)
90   have hb := (PadicInt.norm_int_le_pow_iff_dvd (p := p)).2 hd
91   simpa only [dist_zero_right] using lt_of_le_of_lt hb hN
92 
93 /-- The constructed limit is unique among all p-adic limits of the integer tower. -/
94 theorem compatible_int_tower_unique_limit (p L : ℕ) [Fact p.Prime]
95     (z : ℕ → ℤ)
96     (hstep : ∀ n, (p : ℤ) ^ (L + n) ∣ z (n + 1) - z n) :
97     ∃! a : ℤ_[p],
98       Tendsto (fun n => (z n : ℤ_[p])) atTop (𝓝 a) ∧
99       ∀ n, (p : ℤ_[p]) ^ (L + n) ∣ a - (z n : ℤ_[p]) := by
100   obtain ⟨a, ha, hp⟩ := compatible_int_tower_limit p L z hstep
101   exact ⟨a, ⟨ha, hp⟩, fun b hb => tendsto_nhds_unique hb.1 ha⟩
102 
103 end Komorebi.PadicTowerLimit

Back to source controls