CRT.lean

1 import Mathlib.Data.Nat.Prime.Basic
2 import KomorebiPaperV.Packets
3 
4 /-!
5 Author: Komorebi P.
6 Literal residue-mask factorization using the Chinese remainder equivalence.
7 -/
8 
9 namespace KomorebiPaperV.CRT
10 
11 variable {V : Type*} [Zero V]
12 
13 theorem residue_pair_iff (M N : ℕ) (h : M.Coprime N) (r : ZMod (M * N)) (i : ℤ) :
14     (i : ZMod (M * N)) = r ↔
15       (i : ZMod M) = (ZMod.chineseRemainder h r).1 ∧
16       (i : ZMod N) = (ZMod.chineseRemainder h r).2 := by
17   rw [← (ZMod.chineseRemainder h).injective.eq_iff, Prod.ext_iff]
18   simp only [map_intCast, Prod.fst_intCast, Prod.snd_intCast]
19 
20 theorem residue_mask_factorization (M N : ℕ) (h : M.Coprime N)
21     (r : ZMod (M * N)) (x : ℤ → V) :
22     KomorebiPaperV.packet (fun i : ℤ => (i : ZMod (M * N))) r x =
23       KomorebiPaperV.packet (fun i : ℤ => (i : ZMod M))
24         (ZMod.chineseRemainder h r).1
25         (KomorebiPaperV.packet (fun i : ℤ => (i : ZMod N))
26           (ZMod.chineseRemainder h r).2 x) := by
27   funext i
28   simp only [KomorebiPaperV.packet, residue_pair_iff M N h]
29   split_ifs <;> simp_all
30 
31 theorem dyadic_odd_coprime (a d : ℕ) (hd : Odd d) : (2 ^ a).Coprime d := by
32   exact (Nat.coprime_two_left.mpr hd).pow_left a
33 
34 theorem dyadic_odd_packet_factorization (a d : ℕ) (hd : Odd d)
35     (r : ZMod (2 ^ a * d)) (x : ℤ → V) :
36     KomorebiPaperV.packet (fun i : ℤ => (i : ZMod (2 ^ a * d))) r x =
37       KomorebiPaperV.packet (fun i : ℤ => (i : ZMod (2 ^ a)))
38         (ZMod.chineseRemainder (dyadic_odd_coprime a d hd) r).1
39         (KomorebiPaperV.packet (fun i : ℤ => (i : ZMod d))
40           (ZMod.chineseRemainder (dyadic_odd_coprime a d hd) r).2 x) :=
41   residue_mask_factorization _ _ (dyadic_odd_coprime a d hd) r x
42 
43 end KomorebiPaperV.CRT

Back to source controls