ResidueLiftDigits.lean

1 module
2 public import Mathlib.Data.ZMod.Basic
3 public import Mathlib.Tactic.Ring
4 public import Mathlib.Data.Fintype.Card
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.ResidueLiftDigits
11 
12 variable {d : ℕ}
13 
14 /-- Correction classes modulo q are precisely the classes of shifted integers
15 modulo q^(L+1). This includes q=1 and L=0. -/
16 theorem shift_cast_eq_iff (q L : ℕ) (hq : 0 < q) (x s t : ℤ) :
17     ((x + (q : ℤ)^L * s : ℤ) : ZMod (q^(L+1))) =
18       ((x + (q : ℤ)^L * t : ℤ) : ZMod (q^(L+1))) ↔
19     (s : ZMod q) = (t : ZMod q) := by
20   rw [ZMod.intCast_eq_intCast_iff_dvd_sub,
21     ZMod.intCast_eq_intCast_iff_dvd_sub]
22   have hqL : (q : ℤ)^L ≠ 0 :=
23     pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hq))
24   rw [show (x + (q : ℤ)^L * t) - (x + (q : ℤ)^L * s) =
25     (q : ℤ)^L * (t - s) by ring]
26   rw [Nat.cast_pow, pow_succ, mul_dvd_mul_iff_left hqL]
27 
28 /-- Actual residue vectors at the next level lying over the prescribed
29 integer vector x. The predicate uses canonical integer representatives. -/
30 abbrev ResidueFiber (q L : ℕ) (x : Fin d → ℤ) :=
31   {y : Fin d → ZMod (q^(L+1)) //
32     ∀ i, (q : ℤ)^L ∣ ((y i).val : ℤ) - x i}
33 
34 /-- The actual next residue represented by a correction digit. -/
35 def digitResidue (q L : ℕ) (x : Fin d → ℤ) (t : Fin d → ZMod q) :
36     Fin d → ZMod (q^(L+1)) :=
37   fun i => ((x i + (q : ℤ)^L * ((t i).val : ℤ) : ℤ) : ZMod (q^(L+1)))
38 
39 theorem digitResidue_mem (q L : ℕ) (hq : 0 < q)
40     (x : Fin d → ℤ) (t : Fin d → ZMod q) :
41     ∀ i, (q : ℤ)^L ∣ ((digitResidue q L x t i).val : ℤ) - x i := by
42   let : NeZero (q^(L+1)) := ⟨pow_ne_zero _ (Nat.ne_of_gt hq)⟩
43   intro i
44   have heq : (((digitResidue q L x t i).val : ℤ) : ZMod (q^(L+1))) =
45       ((x i + (q : ℤ)^L * ((t i).val : ℤ) : ℤ) : ZMod (q^(L+1))) := by
46     simp [digitResidue]
47   have hlarge := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ (q^(L+1))).mp heq
48   rw [Nat.cast_pow] at hlarge
49   have hlower : (q : ℤ)^L ∣
50       (x i + (q : ℤ)^L * ((t i).val : ℤ)) - ((digitResidue q L x t i).val : ℤ) :=
51     dvd_trans (pow_dvd_pow (q : ℤ) (Nat.le_succ L)) hlarge
52   have hsum := dvd_sub (dvd_mul_right ((q : ℤ)^L) ((t i).val : ℤ)) hlower
53   have hid : (q : ℤ)^L * ((t i).val : ℤ) -
54       ((x i + (q : ℤ)^L * ((t i).val : ℤ)) - ((digitResidue q L x t i).val : ℤ)) =
55       ((digitResidue q L x t i).val : ℤ) - x i := by ring
56   rwa [hid] at hsum
57 
58 theorem digitResidue_injective (q L : ℕ) (hq : 0 < q) (x : Fin d → ℤ) :
59     Function.Injective (digitResidue q L x) := by
60   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
61   intro s t h
62   funext i
63   have hi := (shift_cast_eq_iff q L hq (x i)
64     ((s i).val : ℤ) ((t i).val : ℤ)).mp (congrFun h i)
65   simpa using hi
66 
67 theorem digitResidue_surjective (q L : ℕ) (hq : 0 < q) (x : Fin d → ℤ)
68     (y : ResidueFiber q L x) :
69     ∃ t : Fin d → ZMod q, digitResidue q L x t = y.val := by
70   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
71   let : NeZero (q^(L+1)) := ⟨pow_ne_zero _ (Nat.ne_of_gt hq)⟩
72   choose s hs using y.property
73   refine ⟨fun i => (s i : ZMod q), ?_⟩
74   funext i
75   have hi := (shift_cast_eq_iff q L hq (x i)
76     (((s i : ZMod q)).val : ℤ) (s i)).mpr (by simp)
77   change digitResidue q L x (fun i => (s i : ZMod q)) i = _ at hi
78   rw [hi]
79   have hy : x i + (q : ℤ)^L * s i = ((y.val i).val : ℤ) := by
80     have hh := hs i
81     exact (sub_eq_iff_eq_add'.mp hh).symm
82   rw [hy]
83   simp
84 
85 /-- All q^d correction digit vectors bijectively parametrize the actual
86 next-level residue vectors over x. Integer corrections themselves are not
87 counted: they have infinitely many representatives. -/
88 def digitEquivResidue (q L : ℕ) (hq : 0 < q) (x : Fin d → ℤ) :
89     (Fin d → ZMod q) ≃ ResidueFiber q L x :=
90   Equiv.ofBijective
91     (fun t => ⟨digitResidue q L x t, digitResidue_mem q L hq x t⟩)
92     ⟨fun _ _ h => digitResidue_injective q L hq x (congrArg Subtype.val h),
93       fun y => by
94         obtain ⟨t, ht⟩ := digitResidue_surjective q L hq x y
95         exact ⟨t, Subtype.ext ht⟩⟩
96 
97 @[simp] theorem digitEquivResidue_apply (q L : ℕ) (hq : 0 < q)
98     (x : Fin d → ℤ) (t : Fin d → ZMod q) :
99     (digitEquivResidue q L hq x t).val = digitResidue q L x t := rfl
100 
101 /-- The canonical representative of an actual digit residue differs from
102 its shifted integer representative by a multiple of the full next modulus. -/
103 theorem next_modulus_dvd_val_sub_shift (q L : ℕ) (hq : 0 < q)
104     (x : Fin d → ℤ) (t : Fin d → ZMod q) (i : Fin d) :
105     (q : ℤ)^(L+1) ∣
106       (((digitEquivResidue q L hq x t).val i).val : ℤ) -
107         (x i + (q : ℤ)^L * ((t i).val : ℤ)) := by
108   let : NeZero (q^(L+1)) := ⟨pow_ne_zero _ (Nat.ne_of_gt hq)⟩
109   have heq : ((x i + (q : ℤ)^L * ((t i).val : ℤ) : ℤ) : ZMod (q^(L+1))) =
110       ((((digitEquivResidue q L hq x t).val i).val : ℤ) : ZMod (q^(L+1))) := by
111     simp [digitEquivResidue_apply, digitResidue]
112   have h := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ (q^(L+1))).mp heq
113   simpa only [Nat.cast_pow] using h
114 
115 /-- Exactly q^d distinct next residue vectors lie above each lower residue,
116 including the degenerate modulus q=1 and the zero-dimensional case. -/
117 theorem residueFiber_card (q L : ℕ) (hq : 0 < q) (x : Fin d → ℤ) :
118     Nat.card (ResidueFiber q L x) = q^d := by
119   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
120   rw [← Nat.card_congr (digitEquivResidue q L hq x)]
121   simp [Nat.card_eq_fintype_card]
122 
123 #print axioms shift_cast_eq_iff
124 #print axioms ResidueFiber
125 #print axioms digitResidue
126 #print axioms digitResidue_mem
127 #print axioms digitResidue_injective
128 #print axioms digitResidue_surjective
129 #print axioms digitEquivResidue
130 #print axioms digitEquivResidue_apply
131 #print axioms next_modulus_dvd_val_sub_shift
132 #print axioms residueFiber_card
133 
134 end Komorebi.ResidueLiftDigits

Back to source controls