DyadicPacketRational.lean

1 module
2 public import DyadicFourLeastPeriods
3 public import Mathlib.NumberTheory.Padics.PadicNorm
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace KomorebiPaperIX.DyadicPacketRational
10 
11 open Congruential DyadicFourLeastPeriods
12 
13 /-- Subtract the constant term and divide by the exact displacement gain. -/
14 def packet (j n : ℕ) : ℚ :=
15   (unnormalized 4 j n - (j.factorial : ℚ)) / (2 : ℚ) ^ originalBonus j
16 
17 @[simp] theorem packet_zero (j : ℕ) : packet j 0 = 0 := by
18   simp [packet, unnormalized]
19 
20 theorem packet_sub (j m n : ℕ) :
21     packet j m - packet j n =
22       (unnormalized 4 j m - unnormalized 4 j n) / (2 : ℚ) ^ originalBonus j := by
23   unfold packet
24   ring
25 
26 /-- Normalization removes exactly the additional valuation, at every row and shift. -/
27 theorem exact_displacement (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
28     packet j (n + T) - packet j n ≠ 0 ∧
29     padicValRat 2 (packet j (n + T) - packet j n) = (padicValNat 2 T : ℤ) := by
30   have h := DyadicFourLeastPeriods.exact_displacement j n T hj hT
31   have hd : (2 : ℚ) ^ originalBonus j ≠ 0 := pow_ne_zero _ (by norm_num)
32   rw [packet_sub]
33   refine ⟨div_ne_zero h.1 hd, ?_⟩
34   rw [padicValRat.div h.1 hd, h.2, padicValRat.pow]
35   rw [show padicValRat 2 (2 : ℚ) = 1 from padicValRat.self (by decide)]
36   ring
37 
38 /-- All positive displacements preserve the dyadic rational norm. -/
39 theorem norm_displacement (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
40     padicNorm 2 (packet j (n + T) - packet j n) = padicNorm 2 (T : ℚ) := by
41   have h := exact_displacement j n T hj hT
42   have ht : (T : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.ne_of_gt hT)
43   rw [padicNorm.eq_zpow_of_nonzero h.1, padicNorm.eq_zpow_of_nonzero ht,
44     h.2, padicValRat.of_nat]
45 
46 /-- The actual rational packets preserve dyadic distance between every pair of rows. -/
47 theorem norm_sub (j m n : ℕ) (hj : j < 4) :
48     padicNorm 2 (packet j m - packet j n) =
49       padicNorm 2 ((m : ℚ) - (n : ℚ)) := by
50   rcases lt_trichotomy m n with hmn | hmn | hmn
51   · have h := norm_displacement j m (n - m) hj (Nat.sub_pos_of_lt hmn)
52     rw [Nat.add_sub_of_le (Nat.le_of_lt hmn), Nat.cast_sub (Nat.le_of_lt hmn)] at h
53     simpa only [← neg_sub (packet j n) (packet j m), padicNorm.neg,
54       ← neg_sub (n : ℚ) (m : ℚ)] using h
55   · subst n
56     simp
57   · have h := norm_displacement j n (m - n) hj (Nat.sub_pos_of_lt hmn)
58     rw [Nat.add_sub_of_le (Nat.le_of_lt hmn), Nat.cast_sub (Nat.le_of_lt hmn)] at h
59     exact h
60 
61 /-- Every normalized packet value is a dyadic integer. -/
62 theorem norm_le_one (j n : ℕ) (hj : j < 4) : padicNorm 2 (packet j n) ≤ 1 := by
63   have h := norm_sub j n 0 hj
64   simp only [packet_zero, sub_zero, Nat.cast_zero] at h
65   rw [h]
66   exact padicNorm.of_nat n
67 
68 end KomorebiPaperIX.DyadicPacketRational

Back to source controls