IntegerPolyphase.lean

1 import KomorebiPaperV.Packets
2 
3 /-!
4 Author: Komorebi P.
5 Checked source; see the bundled build and axiom audit.
6 Literal signed integer polyphase coordinates, with N strictly positive.
7 No summability or Hilbert-space statement is hidden in these pointwise identities.
8 -/
9 
10 open scoped BigOperators
11 namespace KomorebiPaperV.IntegerPolyphase
12 
13 variable {V : Type*}
14 
15 def phase (N : ℕ) (hN : 0 < N) (n : ℤ) : Fin N :=
16   ⟨(n % (N : ℤ)).toNat, by
17     have hn : (N : ℤ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hN)
18     have hlo := Int.emod_nonneg n hn
19     have hhi := Int.emod_lt_of_pos n (show (0 : ℤ) < N by exact_mod_cast hN)
20     omega⟩
21 
22 def quotient (N : ℕ) (n : ℤ) : ℤ := n / (N : ℤ)
23 
24 def address (N : ℕ) (r : Fin N) (q : ℤ) : ℤ := (N : ℤ) * q + (r.val : ℤ)
25 
26 theorem phase_val (N : ℕ) (hN : 0 < N) (n : ℤ) :
27     ((phase N hN n).val : ℤ) = n % (N : ℤ) := by
28   apply Int.toNat_of_nonneg
29   exact Int.emod_nonneg n (by exact_mod_cast (Nat.ne_of_gt hN))
30 
31 theorem address_phase_quotient (N : ℕ) (hN : 0 < N) (n : ℤ) :
32     address N (phase N hN n) (quotient N n) = n := by
33   dsimp [address, quotient]
34   rw [phase_val]
35   exact Int.mul_ediv_add_emod n (N : ℤ)
36 
37 theorem address_divmod (N : ℕ) (hN : 0 < N) (r : Fin N) (q : ℤ) :
38     address N r q / (N : ℤ) = q ∧
39       address N r q % (N : ℤ) = (r.val : ℤ) := by
40   apply (Int.ediv_emod_unique (show (0 : ℤ) < N by exact_mod_cast hN)).mpr
41   refine ⟨?_, ?_, ?_⟩
42   · dsimp [address]
43     ring
44   · exact_mod_cast (Nat.zero_le r.val)
45   · exact_mod_cast r.isLt
46 
47 theorem phase_address (N : ℕ) (hN : 0 < N) (r : Fin N) (q : ℤ) :
48     phase N hN (address N r q) = r := by
49   apply Fin.ext
50   change (address N r q % (N : ℤ)).toNat = r.val
51   rw [(address_divmod N hN r q).2]
52   simp
53 
54 theorem quotient_address (N : ℕ) (hN : 0 < N) (r : Fin N) (q : ℤ) :
55     quotient N (address N r q) = q :=
56   (address_divmod N hN r q).1
57 
58 def addressEquiv (N : ℕ) (hN : 0 < N) : ℤ ≃ Fin N × ℤ where
59   toFun n := (phase N hN n, quotient N n)
60   invFun p := address N p.1 p.2
61   left_inv := address_phase_quotient N hN
62   right_inv p := by
63     apply Prod.ext
64     · exact phase_address N hN p.1 p.2
65     · exact quotient_address N hN p.1 p.2
66 
67 def analysis (N : ℕ) (x : ℤ → V) : Fin N → ℤ → V :=
68   fun r q => x (address N r q)
69 
70 def synthesis (N : ℕ) (hN : 0 < N) (c : Fin N → ℤ → V) : ℤ → V :=
71   fun n => c (phase N hN n) (quotient N n)
72 
73 theorem synthesis_analysis (N : ℕ) (hN : 0 < N) (x : ℤ → V) :
74     synthesis N hN (analysis N x) = x := by
75   funext n
76   exact congrArg x (address_phase_quotient N hN n)
77 
78 theorem analysis_synthesis (N : ℕ) (hN : 0 < N) (c : Fin N → ℤ → V) :
79     analysis N (synthesis N hN c) = c := by
80   funext r q
81   simp only [analysis, synthesis, phase_address N hN, quotient_address N hN]
82 
83 /-- Delay in ORIGINAL sample addresses, allowing negative delays (advances). -/
84 def delay (d : ℤ) (x : ℤ → V) : ℤ → V := fun n => x (n - d)
85 
86 /-- A channel delay d is an original-sample delay N*d. -/
87 theorem channel_delay (N : ℕ) (d : ℤ) (x : ℤ → V) (r : Fin N) (q : ℤ) :
88     analysis N (delay ((N : ℤ) * d) x) r q = analysis N x r (q - d) := by
89   dsimp [analysis, delay, address]
90   congr 1
91   ring
92 
93 /-- General sample delay: the input phase is (r-d) mod N and the carry is signed. -/
94 theorem sample_delay (N : ℕ) (hN : 0 < N) (d : ℤ) (x : ℤ → V)
95     (r : Fin N) (q : ℤ) :
96     analysis N (delay d x) r q =
97       analysis N x (phase N hN ((r.val : ℤ) - d))
98         (q + quotient N ((r.val : ℤ) - d)) := by
99   dsimp [analysis, delay]
100   congr 1
101   have h := address_phase_quotient N hN ((r.val : ℤ) - d)
102   dsimp [address] at h ⊢
103   linear_combination -h
104 
105 /-- Reduction modulo a divisor commutes with reduction modulo the finer modulus. -/
106 theorem emod_coarsen (N M : ℕ) (hNM : N ∣ M) (n : ℤ) :
107     (n % (M : ℤ)) % (N : ℤ) = n % (N : ℤ) := by
108   exact Int.emod_emod_of_dvd n (by exact_mod_cast hNM)
109 
110 /-- Literal integer-residue refinement, before the bounded-operator bridge. -/
111 theorem residue_refinement [AddCommMonoid V] (N M : ℕ) (hN : 0 < N)
112     (hM : 0 < M) (hNM : N ∣ M) (r : Fin N) (x : ℤ → V) (n : ℤ) :
113     KomorebiPaperV.packet (phase N hN) r x n =
114       ∑ s : Fin M, if phase N hN (s.val : ℤ) = r
115         then KomorebiPaperV.packet (phase M hM) s x n else 0 := by
116   have hcoarse : (phase N hN ∘ fun j : ℤ => ((phase M hM j).val : ℤ)) =
117       phase N hN := by
118     funext j
119     apply Fin.ext
120     change (((phase M hM j).val : ℤ) % (N : ℤ)).toNat = (j % (N : ℤ)).toNat
121     rw [phase_val, emod_coarsen N M hNM]
122   have h := KomorebiPaperV.packet_refinement (phase M hM)
123     (fun s : Fin M => phase N hN (s.val : ℤ)) r x n
124   have hc : (fun j : ℤ => phase N hN ((phase M hM j).val : ℤ)) = phase N hN := hcoarse
125   simpa only [Function.comp_def, hc] using h
126 
127 end KomorebiPaperV.IntegerPolyphase

Back to source controls