FIRTransfer.lean

1 import KomorebiPaperV.IntegerPolyphase
2 
3 /-!
4 Author: Komorebi P.
5 Checked source; see the bundled build and axiom audit.
6 Exact finite-support FIR time-domain transfer, including negative tap addresses.
7 All sums below are finite. No bilateral z-transform convergence is assumed.
8 -/
9 
10 open scoped BigOperators
11 namespace KomorebiPaperV.FIRTransfer
12 open KomorebiPaperV.IntegerPolyphase
13 
14 variable {K : Type*} [Semiring K]
15 
16 def reflectEquiv (k : ℤ) : ℤ ≃ ℤ where
17   toFun t := k - t
18   invFun t := k - t
19   left_inv t := by dsimp; omega
20   right_inv t := by dsimp; omega
21 
22 def negateQuotient (N : ℕ) : (Fin N × ℤ) ≃ (Fin N × ℤ) where
23   toFun p := (p.1, -p.2)
24   invFun p := (p.1, -p.2)
25   left_inv p := by cases p; simp
26   right_inv p := by cases p; simp
27 
28 def tapEquiv (N : ℕ) (hN : 0 < N) (k : Fin N) : ℤ ≃ Fin N × ℤ :=
29   ((reflectEquiv (k.val : ℤ)).trans (addressEquiv N hN)).trans (negateQuotient N)
30 
31 def tapIndex (N : ℕ) (k s : Fin N) (m : ℤ) : ℤ :=
32   (N : ℤ) * m + (k.val : ℤ) - (s.val : ℤ)
33 
34 theorem tapEquiv_symm (N : ℕ) (hN : 0 < N) (k s : Fin N) (m : ℤ) :
35     (tapEquiv N hN k).symm (s, m) = tapIndex N k s m := by
36   simp only [tapEquiv, Equiv.symm_trans_apply, reflectEquiv,
37     addressEquiv, negateQuotient, Equiv.coe_fn_symm_mk,
38     address, tapIndex]
39   ring
40 
41 theorem tapIndex_equiv (N : ℕ) (hN : 0 < N) (k : Fin N) (t : ℤ) :
42     tapIndex N k ((tapEquiv N hN k) t).1 ((tapEquiv N hN k) t).2 = t := by
43   calc
44     _ = (tapEquiv N hN k).symm ((tapEquiv N hN k) t) :=
45       (tapEquiv_symm N hN k _ _).symm
46     _ = t := (tapEquiv N hN k).symm_apply_apply t
47 
48 theorem transfer_address (N : ℕ) (k s : Fin N) (n m : ℤ) :
49     address N k n - tapIndex N k s m = address N s (n - m) := by
50   dsimp [address, tapIndex]
51   ring
52 
53 def fir (h : ℤ →₀ K) (x : ℤ → K) (n : ℤ) : K :=
54   ∑ t ∈ h.support, h t * x (n - t)
55 
56 def kernel (N : ℕ) (h : ℤ →₀ K) (k s : Fin N) (m : ℤ) : K :=
57   h (tapIndex N k s m)
58 
59 def transferSupport (N : ℕ) (hN : 0 < N) (h : ℤ →₀ K) (k : Fin N) :
60     Finset (Fin N × ℤ) := h.support.map (tapEquiv N hN k).toEmbedding
61 
62 def delays (N : ℕ) (hN : 0 < N) (h : ℤ →₀ K) (k s : Fin N) : Finset ℤ :=
63   ((transferSupport N hN h k).filter (fun p => p.1 = s)).image Prod.snd
64 
65 theorem fir_reindex (N : ℕ) (hN : 0 < N) (h : ℤ →₀ K) (x : ℤ → K)
66     (k : Fin N) (n : ℤ) :
67     fir h x (address N k n) =
68       ∑ p ∈ transferSupport N hN h k,
69         kernel N h k p.1 p.2 * analysis N x p.1 (n - p.2) := by
70   simp only [fir, transferSupport, Finset.sum_map]
71   apply Finset.sum_congr rfl
72   intro t _
73   dsimp only [Function.Embedding.coeFn_mk, Equiv.toEmbedding, kernel, analysis]
74   have ht := tapIndex_equiv N hN k t
75   rw [ht]
76   congr 1
77   apply congrArg x
78   exact (congrArg (fun t' => address N k n - t') ht.symm).trans
79     (transfer_address N k _ n _)
80 
81 /-- Reindex a fiber of a finite set of pairs by its second coordinate. -/
82 theorem sum_pair_fiber {R Q E : Type*} [DecidableEq R] [DecidableEq Q]
83     [AddCommMonoid E] (u : Finset (R × Q)) (r : R) (F : R → Q → E) :
84     (∑ p ∈ u.filter (fun p => p.1 = r), F p.1 p.2) =
85       ∑ q ∈ (u.filter (fun p => p.1 = r)).image Prod.snd, F r q := by
86   rw [Finset.sum_image (by
87     intro p hp q hq hpq
88     apply Prod.ext
89     · exact (Finset.mem_filter.mp hp).2.trans (Finset.mem_filter.mp hq).2.symm
90     · exact hpq)]
91   apply Finset.sum_congr rfl
92   intro p hp
93   rw [(Finset.mem_filter.mp hp).2]
94 
95 /-- Literal h[k,s](m)=h[N*m+k-s] transfer, on the exact finite channel supports. -/
96 theorem fir_polyphase_transfer (N : ℕ) (hN : 0 < N) (h : ℤ →₀ K)
97     (x : ℤ → K) (k : Fin N) (n : ℤ) :
98     analysis N (fir h x) k n =
99       ∑ s : Fin N, ∑ m ∈ delays N hN h k s,
100         kernel N h k s m * analysis N x s (n - m) := by
101   change fir h x (address N k n) = _
102   rw [fir_reindex N hN h x k n]
103   calc
104     _ = ∑ s : Fin N, ∑ p ∈ (transferSupport N hN h k).filter (fun p => p.1 = s),
105         kernel N h k p.1 p.2 * analysis N x p.1 (n - p.2) :=
106       (Finset.sum_fiberwise (transferSupport N hN h k) Prod.fst
107         (fun p => kernel N h k p.1 p.2 * analysis N x p.1 (n - p.2))).symm
108     _ = _ := by
109       apply Finset.sum_congr rfl
110       intro s _
111       exact sum_pair_fiber (transferSupport N hN h k) s
112         (fun r m => kernel N h k r m * analysis N x r (n - m))
113 
114 end KomorebiPaperV.FIRTransfer

Back to source controls