HilbertPackets.lean

1 import Mathlib.Analysis.InnerProductSpace.l2Space
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.Analysis.Normed.Lp.lpSpace
4 import KomorebiPaperV.IntegerPolyphase
5 
6 /-!
7 Author: Komorebi P.
8 Square-summable signals: bounded packet maps, exact synthesis, and isometric
9 integer address coordinates. The channel target uses the joint l2 norm on
10 Fin N × Z, rather than the supremum norm on a function space of channels.
11 -/
12 
13 open scoped BigOperators
14 namespace KomorebiPaperV.HilbertPackets
15 
16 abbrev Signal (I : Type*) : Type _ := lp (fun _ : I => ℂ) 2
17 
18 variable {I R S J : Type*}
19 
20 noncomputable def projection [DecidableEq R] (phase : I → R) (r : R)
21     (x : Signal I) : Signal I :=
22   ⟨KomorebiPaperV.packet phase r x, (lp.memℓp x).mono' (by
23     intro i
24     by_cases h : phase i = r <;> simp [KomorebiPaperV.packet, h])⟩
25 
26 theorem projection_apply [DecidableEq R] (phase : I → R) (r : R)
27     (x : Signal I) (i : I) :
28     projection phase r x i = if phase i = r then x i else 0 := rfl
29 
30 theorem projection_norm_le [DecidableEq R] (phase : I → R) (r : R)
31     (x : Signal I) : ‖projection phase r x‖ ≤ ‖x‖ := by
32   apply lp.norm_mono (by norm_num)
33   intro i
34   by_cases h : phase i = r <;> simp [projection_apply, h]
35 
36 noncomputable def projectionLinear [DecidableEq R] (phase : I → R) (r : R) :
37     Signal I →ₗ[ℂ] Signal I where
38   toFun := projection phase r
39   map_add' x y := by
40     ext i
41     by_cases h : phase i = r <;> simp [projection_apply, h]
42   map_smul' a x := by
43     ext i
44     by_cases h : phase i = r <;> simp [projection_apply, h]
45 
46 noncomputable def projector [DecidableEq R] (phase : I → R) (r : R) :
47     Signal I →L[ℂ] Signal I :=
48   (projectionLinear phase r).mkContinuous 1 (by
49     intro x
50     change ‖projection phase r x‖ ≤ 1 * ‖x‖
51     simpa using projection_norm_le phase r x)
52 
53 theorem projector_apply [DecidableEq R] (phase : I → R) (r : R)
54     (x : Signal I) : projector phase r x = projection phase r x := rfl
55 
56 theorem projector_idempotent [DecidableEq R] (phase : I → R) (r : R) :
57     (projector phase r).comp (projector phase r) = projector phase r := by
58   ext x i
59   by_cases h : phase i = r <;>
60     simp [projector_apply, projection_apply, h]
61 
62 theorem projector_annihilate [DecidableEq R] (phase : I → R) (r s : R) (h : r ≠ s) :
63     (projector phase r).comp (projector phase s) = 0 := by
64   ext x i
65   by_cases hr : phase i = r
66   · simp [projector_apply, projection_apply, hr, h]
67   · simp [projector_apply, projection_apply, hr]
68 
69 theorem projector_complete [Fintype R] [DecidableEq R] (phase : I → R) :
70     (∑ r : R, projector phase r) = ContinuousLinearMap.id ℂ (Signal I) := by
71   apply ContinuousLinearMap.ext
72   intro x
73   simp only [sum_apply, ContinuousLinearMap.id_apply, projector_apply]
74   apply lp.ext
75   funext i
76   simp only [lp.coeFn_sum, Finset.sum_apply, projection_apply]
77   exact KomorebiPaperV.packet_complete phase (fun j => x j) i
78 
79 theorem projector_refinement [Fintype S] [DecidableEq S] [DecidableEq R]
80     (fine : I → S) (coarsen : S → R) (r : R) :
81     projector (coarsen ∘ fine) r =
82       ∑ s : S, if coarsen s = r then projector fine s else 0 := by
83   apply ContinuousLinearMap.ext
84   intro x
85   simp only [sum_apply, projector_apply]
86   apply lp.ext
87   funext i
88   rw [lp.coeFn_sum, Finset.sum_apply]
89   calc
90     _ = ∑ s : S, if coarsen s = r then projection fine s x i else 0 :=
91       KomorebiPaperV.packet_refinement fine coarsen r (fun j => x j) i
92     _ = _ := by
93       apply Finset.sum_congr rfl
94       intro s _
95       by_cases h : coarsen s = r <;> simp [h, projector_apply]
96 
97 noncomputable def reindex (e : I ≃ J) (x : Signal I) : Signal J :=
98   ⟨fun j => x (e.symm j), memℓp_gen (by
99     simpa only [Function.comp_def] using
100       e.symm.summable_iff.mpr ((lp.memℓp x).summable (by norm_num)))⟩
101 
102 theorem reindex_norm (e : I ≃ J) (x : Signal I) : ‖reindex e x‖ = ‖x‖ := by
103   rw [lp.norm_eq_tsum_rpow (by norm_num), lp.norm_eq_tsum_rpow (by norm_num)]
104   congr 1
105   exact e.symm.tsum_eq (fun i => ‖x i‖ ^ (2 : ENNReal).toReal)
106 
107 noncomputable def reindexIsometry (e : I ≃ J) : Signal I ≃ₗᵢ[ℂ] Signal J where
108   toFun := reindex e
109   invFun := reindex e.symm
110   left_inv x := by ext i; simp [reindex]
111   right_inv x := by ext j; simp [reindex]
112   map_add' x y := by ext j; rfl
113   map_smul' a x := by ext j; rfl
114   norm_map' := reindex_norm e
115 
116 noncomputable def polyphase (N : ℕ) (hN : 0 < N) :
117     Signal ℤ ≃ₗᵢ[ℂ] Signal (Fin N × ℤ) :=
118   reindexIsometry (KomorebiPaperV.IntegerPolyphase.addressEquiv N hN)
119 
120 theorem polyphase_apply (N : ℕ) (hN : 0 < N) (x : Signal ℤ) (r : Fin N) (q : ℤ) :
121     polyphase N hN x (r, q) = x ((N : ℤ) * q + (r.val : ℤ)) := rfl
122 
123 theorem polyphase_synthesis_analysis (N : ℕ) (hN : 0 < N) (x : Signal ℤ) :
124     (polyphase N hN).symm (polyphase N hN x) = x :=
125   (polyphase N hN).symm_apply_apply x
126 
127 theorem polyphase_analysis_synthesis (N : ℕ) (hN : 0 < N) (x : Signal (Fin N × ℤ)) :
128     polyphase N hN ((polyphase N hN).symm x) = x :=
129   (polyphase N hN).apply_symm_apply x
130 
131 theorem polyphase_energy (N : ℕ) (hN : 0 < N) (x : Signal ℤ) :
132     ‖polyphase N hN x‖ ^ 2 = ‖x‖ ^ 2 := by
133   rw [(polyphase N hN).norm_map]
134 
135 theorem impulse_expansion (x : Signal ℤ) :
136     HasSum (fun i : ℤ => lp.single 2 i (x i)) x :=
137   lp.hasSum_single (by norm_num) x
138 
139 theorem projector_symmetric [DecidableEq R] (phase : I → R) (r : R)
140     (x y : Signal I) :
141     inner ℂ (projector phase r x) y = inner ℂ x (projector phase r y) := by
142   rw [lp.inner_eq_tsum, lp.inner_eq_tsum]
143   apply tsum_congr
144   intro i
145   by_cases h : phase i = r <;> simp [projector_apply, projection_apply, h]
146 
147 theorem projector_orthogonal [DecidableEq R] (phase : I → R) (r s : R)
148     (h : r ≠ s) (x y : Signal I) :
149     inner ℂ (projector phase r x) (projector phase s y) = 0 := by
150   rw [lp.inner_eq_tsum]
151   have hz : ∀ i, inner ℂ (projector phase r x i) (projector phase s y i) = 0 := by
152     intro i
153     by_cases hr : phase i = r
154     · simp [projector_apply, projection_apply, hr, h]
155     · simp [projector_apply, projection_apply, hr]
156   simp only [hz, tsum_zero]
157 
158 noncomputable def impulseBasis : HilbertBasis ℤ ℂ (Signal ℤ) :=
159   ⟨LinearIsometryEquiv.refl ℂ (Signal ℤ)⟩
160 
161 theorem impulse_basis_apply (i : ℤ) : impulseBasis i = lp.single 2 i (1 : ℂ) := by
162   rw [← impulseBasis.repr_symm_single]
163   rfl
164 
165 theorem impulse_dense_span :
166     (Submodule.span ℂ (Set.range (fun i : ℤ => (lp.single 2 i (1 : ℂ) : Signal ℤ)))).topologicalClosure = ⊤ := by
167   have hfun : (⇑impulseBasis : ℤ → Signal ℤ) = fun i => lp.single 2 i (1 : ℂ) :=
168     funext impulse_basis_apply
169   rw [← hfun]
170   exact impulseBasis.dense_span
171 
172 noncomputable def shift (d : ℤ) : Signal ℤ ≃ₗᵢ[ℂ] Signal ℤ :=
173   reindexIsometry (Equiv.addRight d)
174 
175 theorem shift_apply (d n : ℤ) (x : Signal ℤ) : shift d x n = x (n - d) := rfl
176 
177 theorem reindex_single (e : I ≃ J) [DecidableEq I] [DecidableEq J] (i : I) (c : ℂ) :
178     reindex e (lp.single 2 i c) = lp.single 2 (e i) c := by
179   apply lp.ext
180   funext j
181   simp [reindex, lp.single_apply, Pi.single_apply, Equiv.symm_apply_eq]
182 
183 theorem shift_impulse (d i : ℤ) :
184     shift d (lp.single 2 i (1 : ℂ)) = lp.single 2 (i + d) (1 : ℂ) :=
185   reindex_single (Equiv.addRight d) i 1
186 
187 theorem residue_projector_refinement (N M : ℕ) (hN : 0 < N) (hM : 0 < M)
188     (hNM : N ∣ M) (r : Fin N) :
189     projector (IntegerPolyphase.phase N hN) r =
190       ∑ s : Fin M, if IntegerPolyphase.phase N hN (s.val : ℤ) = r
191         then projector (IntegerPolyphase.phase M hM) s else 0 := by
192   have hc : (fun j : ℤ => IntegerPolyphase.phase N hN
193       ((IntegerPolyphase.phase M hM j).val : ℤ)) = IntegerPolyphase.phase N hN := by
194     funext j
195     apply Fin.ext
196     change (((IntegerPolyphase.phase M hM j).val : ℤ) % (N : ℤ)).toNat =
197       (j % (N : ℤ)).toNat
198     rw [IntegerPolyphase.phase_val, IntegerPolyphase.emod_coarsen N M hNM]
199   have h := projector_refinement (IntegerPolyphase.phase M hM)
200     (fun s : Fin M => IntegerPolyphase.phase N hN (s.val : ℤ)) r
201   simpa only [Function.comp_def, hc] using h
202 
203 theorem shift_generated_dense_span :
204     (Submodule.span ℂ (Set.range (fun i : ℤ => shift i (lp.single 2 0 (1 : ℂ))))).topologicalClosure = ⊤ := by
205   simpa only [shift_impulse, zero_add] using impulse_dense_span
206 
207 theorem finite_impulse_expansion (s : Finset ℤ) (x : Signal ℤ)
208     (hs : ∀ i ∉ s, x i = 0) : (∑ i ∈ s, lp.single 2 i (x i)) = x := by
209   have hsum : HasSum (fun i : ℤ => (lp.single 2 i (x i) : Signal ℤ))
210       (∑ i ∈ s, lp.single 2 i (x i)) :=
211     hasSum_sum_of_ne_finset_zero (fun i hi => by rw [hs i hi, lp.single_zero])
212   exact hsum.unique (impulse_expansion x)
213 
214 end KomorebiPaperV.HilbertPackets

Back to source controls