RationalPadicEmbedding.lean

1 module
2 public import Mathlib.NumberTheory.Padics.PadicIntegers
3 
4 /-!
5 # Rational samples as p-adic integer samples
6 
7 Author: Komorebi P.
8 The natural input metric is the metric inherited from the p-adic integers.
9 No claim identifies it with the usual metric on the natural numbers.
10 -/
11 
12 @[expose] public section
13 noncomputable section
14 set_option autoImplicit false
15 
16 namespace KomorebiPaperIX.RationalPadicEmbedding
17 
18 variable (p : ℕ) [Fact p.Prime]
19 
20 theorem norm_le_one (f : ℕ → ℚ) (h0 : f 0 = 0)
21     (h : ∀ m n, padicNorm p (f m - f n) = padicNorm p ((m : ℚ) - n)) (n : ℕ) :
22     ‖(f n : ℚ_[p])‖ ≤ 1 := by
23   have hn : padicNorm p (f n) = padicNorm p (n : ℚ) := by
24     simpa only [h0, Nat.cast_zero, sub_zero] using h n 0
25   rw [Padic.eq_padicNorm, hn]
26   have hi : ‖((n : ℚ) : ℚ_[p])‖ ≤ 1 := by
27     simpa only [Rat.cast_natCast, Int.cast_natCast] using
28       Padic.norm_int_le_one (p := p) (n : ℤ)
29   simpa only [Padic.eq_padicNorm] using hi
30 
31 /-- The exact rational values, included in the integral unit ball. -/
32 def samples (f : ℕ → ℚ) (h0 : f 0 = 0)
33     (h : ∀ m n, padicNorm p (f m - f n) = padicNorm p ((m : ℚ) - n)) :
34     ℕ → ℤ_[p] :=
35   fun n => ⟨(f n : ℚ_[p]), norm_le_one p f h0 h n⟩
36 
37 @[simp]
38 theorem samples_coe (f : ℕ → ℚ) (h0 : f 0 = 0)
39     (h : ∀ m n, padicNorm p (f m - f n) = padicNorm p ((m : ℚ) - n)) (n : ℕ) :
40     (samples p f h0 h n : ℚ_[p]) = (f n : ℚ_[p]) := rfl
41 
42 /-- Distances agree with natural numbers embedded in the p-adic integers. -/
43 theorem samples_dist (f : ℕ → ℚ) (h0 : f 0 = 0)
44     (h : ∀ m n, padicNorm p (f m - f n) = padicNorm p ((m : ℚ) - n)) (m n : ℕ) :
45     dist (samples p f h0 h m) (samples p f h0 h n) =
46       dist (m : ℤ_[p]) (n : ℤ_[p]) := by
47   simp only [dist_eq_norm, PadicInt.norm_def, PadicInt.coe_sub, samples_coe,
48     PadicInt.coe_natCast]
49   have hm : (m : ℚ_[p]) = ((m : ℚ) : ℚ_[p]) := by simp
50   have hn : (n : ℚ_[p]) = ((n : ℚ) : ℚ_[p]) := by simp
51   rw [hm, hn, ← Rat.cast_sub, ← Rat.cast_sub, Padic.eq_padicNorm, Padic.eq_padicNorm, h]
52 
53 end KomorebiPaperIX.RationalPadicEmbedding
54 
55 #print axioms KomorebiPaperIX.RationalPadicEmbedding.norm_le_one
56 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples
57 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples_coe
58 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples_dist

Back to source controls