FilterBank.lean

1 import KomorebiPaperV.ZTransform
2 import Mathlib.Algebra.MonoidAlgebra.Basic
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 
5 /-!
6 Author: Komorebi P. FIR banks as matrices of finite Laurent polynomials.
7 A monomial at d is z^(-d), acting by x[n] ↦ x[n-d]. The matrix criterion is
8 proved on all bilateral sequences, without a convergence assumption.
9 -/
10 namespace KomorebiPaperV.FilterBank
11 abbrev Signal := ℤ → ℂ
12 abbrev Laurent := AddMonoidAlgebra ℂ ℤ
13 
14 noncomputable def delayMap (d : ℤ) : Module.End ℂ Signal where
15   toFun x := fun n => x (n-d)
16   map_add' _ _ := rfl
17   map_smul' _ _ := rfl
18 
19 noncomputable def shiftHom : Multiplicative ℤ →* Module.End ℂ Signal where
20   toFun d := delayMap d.toAdd
21   map_one' := by ext x n; change x (n-0) = x n; simp
22   map_mul' a b := by
23     ext x n
24     change x (n-(a.toAdd+b.toAdd)) = x (n-a.toAdd-b.toAdd)
25     congr 1
26     ring
27 
28 noncomputable def act : Laurent →ₐ[ℂ] Module.End ℂ Signal :=
29   AddMonoidAlgebra.lift ℂ (Module.End ℂ Signal) ℤ shiftHom
30 
31 theorem act_apply (h : Laurent) (x : Signal) (n : ℤ) :
32     act h x n = ∑ t ∈ h.coeff.support, h.coeff t * x (n-t) := by
33   rw [act, AddMonoidAlgebra.lift_apply]
34   simp [Finsupp.sum, shiftHom, delayMap]
35 
36 theorem act_is_fir (h : Laurent) (x : Signal) :
37     act h x = KomorebiPaperV.FIRTransfer.fir h.coeff x := by
38   funext n
39   exact act_apply h x n
40 
41 noncomputable def impulse : Signal := fun n => if n = 0 then 1 else 0
42 
43 theorem act_impulse (h : Laurent) (n : ℤ) : act h impulse n = h.coeff n := by
44   classical
45   rw [act_apply]
46   simp [impulse, sub_eq_zero, Finsupp.mem_support_iff]
47   intro hzero
48   exact hzero.symm
49 
50 theorem act_single (d : ℤ) (c : ℂ) (x : Signal) (n : ℤ) :
51     act (AddMonoidAlgebra.single d c) x n = c * x (n-d) := by
52   rw [act, AddMonoidAlgebra.lift_single]
53   rfl
54 
55 noncomputable def scalarShift (z : ℂ) (hz : z ≠ 0) : Multiplicative ℤ →* ℂ where
56   toFun d := z ^ (-d.toAdd)
57   map_one' := by simp
58   map_mul' a b := by
59     change z ^ (-(a.toAdd+b.toAdd)) = z ^ (-a.toAdd) * z ^ (-b.toAdd)
60     rw [neg_add, zpow_add₀ hz]
61 
62 noncomputable def evalZ (z : ℂ) (hz : z ≠ 0) : Laurent →ₐ[ℂ] ℂ :=
63   AddMonoidAlgebra.lift ℂ ℂ ℤ (scalarShift z hz)
64 
65 theorem evalZ_apply (z : ℂ) (hz : z ≠ 0) (h : Laurent) :
66     evalZ z hz h = ∑ d ∈ h.coeff.support, h.coeff d * z ^ (-d) := by
67   rw [evalZ, AddMonoidAlgebra.lift_apply]
68   rfl
69 
70 theorem filter_transform (h : Laurent) (x : Signal) (z X : ℂ) (hz : z ≠ 0)
71     (hx : KomorebiPaperV.ZTransform.HasTransform x z X) :
72     KomorebiPaperV.ZTransform.HasTransform (act h x) z (evalZ z hz h * X) := by
73   have ht := KomorebiPaperV.ZTransform.finite_transfer_transform h.coeff.support
74     (fun _ => x) (fun d => h.coeff d) (fun d => d) z hz (fun _ => X) (fun _ _ => hx)
75   simpa only [KomorebiPaperV.ZTransform.HasTransform, act_apply, evalZ_apply,
76     Finset.sum_mul] using ht
77 
78 variable {I : Type*} [Fintype I] [DecidableEq I]
79 
80 noncomputable def bank (B : Matrix I I Laurent) (x : I → Signal) : I → Signal :=
81   fun k => ∑ s, act (B k s) (x s)
82 
83 omit [DecidableEq I] in
84 theorem bank_mul (A B : Matrix I I Laurent) (x : I → Signal) :
85     bank (A*B) x = bank A (bank B x) := by
86   funext k
87   simp only [bank, Matrix.mul_apply, map_sum, map_mul, LinearMap.sum_apply,
88     Module.End.mul_apply]
89   rw [Finset.sum_comm]
90 
91 noncomputable def channelImpulse (s : I) : I → Signal := Pi.single s impulse
92 
93 theorem bank_impulse (B : Matrix I I Laurent) (k s : I) (n : ℤ) :
94     bank B (channelImpulse s) k n = (B k s).coeff n := by
95   classical
96   simp only [bank, channelImpulse, Pi.single_apply, Finset.sum_apply]
97   rw [Finset.sum_eq_single s]
98   · simpa only [↓reduceIte] using act_impulse (B k s) n
99   · intro j _ hj
100     simp only [ite_eq_right hj, map_zero, Pi.zero_apply]
101   · intro hs
102     exact False.elim (hs (Finset.mem_univ s))
103 
104 theorem bank_faithful (A B : Matrix I I Laurent) :
105     (∀ x, bank A x = bank B x) ↔ A = B := by
106   constructor
107   · intro h
108     funext k s
109     apply AddMonoidAlgebra.ext
110     apply Finsupp.ext
111     intro n
112     have he := congrArg (fun y : I → Signal => y k n) (h (channelImpulse s))
113     simpa only [bank_impulse] using he
114   · rintro rfl
115     intro x
116     rfl
117 
118 noncomputable def gainDelay (c : ℂ) (d : ℤ) : Matrix I I Laurent :=
119   Matrix.diagonal (fun _ => AddMonoidAlgebra.single d c)
120 
121 theorem gain_delay_action (c : ℂ) (d : ℤ) (x : I → Signal) (k : I) (n : ℤ) :
122     bank (gainDelay c d) x k n = c*x k (n-d) := by
123   classical
124   simp only [bank, gainDelay, Matrix.diagonal_apply, Finset.sum_apply]
125   rw [Finset.sum_eq_single k]
126   · simpa only [↓reduceIte] using act_single d c (x k) n
127   · intro j _ hj
128     simp only [ite_eq_right hj.symm, map_zero, LinearMap.zero_apply, Pi.zero_apply]
129   · intro hk
130     exact False.elim (hk (Finset.mem_univ k))
131 
132 /-- Exact reconstruction of every channel sequence iff the Laurent matrix is gain times delay. -/
133 theorem perfect_reconstruction_iff (E R : Matrix I I Laurent) (c : ℂ) (d : ℤ) :
134     (∀ x : I → Signal, ∀ k n, bank R (bank E x) k n = c*x k (n-d)) ↔
135       R*E = gainDelay c d := by
136   rw [← bank_faithful]
137   constructor
138   · intro h x
139     funext k n
140     rw [bank_mul, gain_delay_action]
141     exact h x k n
142   · intro h x k n
143     have he := congrArg (fun y : I → Signal => y k n) (h x)
144     simpa only [bank_mul, gain_delay_action] using he
145 
146 omit [DecidableEq I] in
147 theorem bank_transform (B : Matrix I I Laurent) (x : I → Signal) (z : ℂ) (hz : z ≠ 0)
148     (X : I → ℂ) (hx : ∀ i, KomorebiPaperV.ZTransform.HasTransform (x i) z (X i)) (k : I) :
149     KomorebiPaperV.ZTransform.HasTransform (bank B x k) z
150       (Matrix.mulVec (fun k s => evalZ z hz (B k s)) X k) := by
151   have ht := hasSum_sum (s := Finset.univ) (fun s _ => filter_transform (B k s) (x s) z (X s) hz (hx s))
152   simpa only [KomorebiPaperV.ZTransform.HasTransform, bank, Finset.sum_apply,
153     Finset.sum_mul, Matrix.mulVec, dotProduct] using ht
154 
155 theorem original_sample_delay (N : ℕ) (hN : 0 < N)
156     (E R : Matrix (Fin N) (Fin N) Laurent) (c : ℂ) (d : ℤ)
157     (h : R*E = gainDelay c d) (x : Signal) (n : ℤ) :
158     KomorebiPaperV.IntegerPolyphase.synthesis N hN
159       (bank R (bank E (KomorebiPaperV.IntegerPolyphase.analysis N x))) n = c*x (n-(N:ℤ)*d) := by
160   have hr := (perfect_reconstruction_iff E R c d).mpr h
161   unfold KomorebiPaperV.IntegerPolyphase.synthesis
162   rw [hr]
163   congr 1
164   unfold KomorebiPaperV.IntegerPolyphase.analysis
165   congr 1
166   have ha := KomorebiPaperV.IntegerPolyphase.address_phase_quotient N hN n
167   dsimp [KomorebiPaperV.IntegerPolyphase.address] at ha ⊢
168   linarith
169 
170 end KomorebiPaperV.FilterBank

Back to source controls