ZTransform.lean

1 import KomorebiPaperV.FIRTransfer
2 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 
5 /-!
6 Author: Komorebi P. Bilateral channel transforms with explicit summability.
7 The time-domain FIR theorem applies to every sequence. A transform equality is
8 asserted only where the input weighted series converges; no totalized divergent
9 series is silently treated as a transform.
10 -/
11 namespace KomorebiPaperV.ZTransform
12 open KomorebiPaperV.FIRTransfer KomorebiPaperV.IntegerPolyphase
13 
14 noncomputable def transform (x : ℤ → ℂ) (z : ℂ) : ℂ := ∑' n, x n * z ^ (-n)
15 
16 def HasTransform (x : ℤ → ℂ) (z X : ℂ) : Prop := HasSum (fun n => x n * z ^ (-n)) X
17 
18 theorem transform_unique (x : ℤ → ℂ) (z X : ℂ) (h : HasTransform x z X) :
19     transform x z = X := h.tsum_eq
20 
21 theorem delay_transform (x : ℤ → ℂ) (z X : ℂ) (hz : z ≠ 0)
22     (h : HasTransform x z X) (d : ℤ) :
23     HasTransform (fun n => x (n-d)) z (z ^ (-d) * X) := by
24   have hh := h.mul_left (z ^ (-d))
25   have he : (fun n : ℤ => z ^ (-d) * (x n * z ^ (-n))) =
26       (fun n : ℤ => x (n-d) * z ^ (-n)) ∘ Equiv.addRight d := by
27     funext n
28     change z ^ (-d) * (x n * z ^ (-n)) = x (n+d-d) * z ^ (-(n+d))
29     rw [add_sub_cancel_right, neg_add, zpow_add₀ hz]
30     ring
31   rw [he] at hh
32   exact (Equiv.addRight d).hasSum_iff.mp hh
33 
34 theorem finite_transfer_transform {I : Type*} (s : Finset I) (x : I → ℤ → ℂ)
35     (w : I → ℂ) (d : I → ℤ) (z : ℂ) (hz : z ≠ 0) (X : I → ℂ)
36     (hx : ∀ i ∈ s, HasTransform (x i) z (X i)) :
37     HasTransform (fun n => ∑ i ∈ s, w i * x i (n-d i)) z
38       (∑ i ∈ s, w i * z ^ (-d i) * X i) := by
39   have hh : ∀ i ∈ s, HasSum (fun n => w i * (x i (n-d i) * z ^ (-n)))
40       (w i * (z ^ (-d i) * X i)) :=
41     fun i hi => (delay_transform (x i) z (X i) hz (hx i hi) (d i)).mul_left (w i)
42   have ht := hasSum_sum hh
43   simpa [HasTransform, Finset.sum_mul, mul_assoc] using ht
44 
45 noncomputable def transferMatrix (N : ℕ) (hN : 0 < N) (h : ℤ →₀ ℂ) (z : ℂ) :
46     Matrix (Fin N) (Fin N) ℂ := fun k s =>
47   ∑ m ∈ delays N hN h k s, kernel N h k s m * z ^ (-m)
48 
49 theorem fir_channel_transform (N : ℕ) (hN : 0 < N) (h : ℤ →₀ ℂ) (x : ℤ → ℂ)
50     (z : ℂ) (hz : z ≠ 0) (X : Fin N → ℂ)
51     (hx : ∀ s, HasTransform (analysis N x s) z (X s)) (k : Fin N) :
52     HasTransform (analysis N (fir h x) k) z ((transferMatrix N hN h z).mulVec X k) := by
53   have hh : ∀ s : Fin N, HasSum
54       (fun n => (∑ m ∈ delays N hN h k s, kernel N h k s m * analysis N x s (n-m)) * z ^ (-n))
55       (transferMatrix N hN h z k s * X s) := by
56     intro s
57     have ht := finite_transfer_transform (delays N hN h k s) (fun _ => analysis N x s)
58       (fun m => kernel N h k s m) (fun m => m) z hz (fun _ => X s) (fun _ _ => hx s)
59     simpa [HasTransform, transferMatrix, Finset.sum_mul] using ht
60   have ht := hasSum_sum (s := Finset.univ) (fun s _ => hh s)
61   simpa only [HasTransform, fir_polyphase_transfer N hN h x, Finset.sum_mul,
62     Matrix.mulVec, dotProduct] using ht
63 
64 theorem fir_matrix_transform (N : ℕ) (hN : 0 < N) (h : ℤ →₀ ℂ) (x : ℤ → ℂ)
65     (z : ℂ) (hz : z ≠ 0)
66     (hx : ∀ s, Summable (fun n => analysis N x s n * z ^ (-n))) :
67     (fun k => transform (analysis N (fir h x) k) z) =
68       (transferMatrix N hN h z).mulVec (fun s => transform (analysis N x s) z) := by
69   funext k
70   exact (fir_channel_transform N hN h x z hz _ (fun s => (hx s).hasSum) k).tsum_eq
71 
72 end KomorebiPaperV.ZTransform

Back to source controls