HaarChannels.lean

1 import KomorebiPaperV.HaarHilbert
2 
3 /-! Author: Komorebi P. Literal interleaved l2 channels and the Haar energy theorem. -/
4 namespace KomorebiPaperV.HaarChannels
5 open KomorebiPaperV.HilbertPackets KomorebiPaperV.HaarHilbert
6 
7 noncomputable def channel {I J : Type*} (x : Signal (I × J)) (i : I) : Signal J :=
8   ⟨fun j => x (i,j), memℓp_gen (by
9     exact ((lp.memℓp x).summable (by norm_num)).comp_injective
10       (fun _ _ h => Prod.mk.inj h |>.2))⟩
11 
12 theorem norm_sq_tsum {I : Type*} (x : Signal I) : ‖x‖ ^ 2 = ∑' i, ‖x i‖ ^ 2 := by
13   simpa using lp.norm_rpow_eq_tsum (by norm_num : 0 < (2 : ENNReal).toReal) x
14 
15 theorem channel_energy {I J : Type*} [Fintype I] (x : Signal (I × J)) :
16     ∑ i, ‖channel x i‖ ^ 2 = ‖x‖ ^ 2 := by
17   simp_rw [norm_sq_tsum]
18   have hs : Summable (fun p : I × J => ‖x p‖ ^ 2) := by
19     simpa using (lp.memℓp x).summable (by norm_num)
20   rw [hs.tsum_prod]
21   exact (tsum_fintype _).symm
22 
23 noncomputable def even (x : Signal ℤ) : Signal ℤ := channel (polyphase 2 (by norm_num) x) 0
24 noncomputable def odd (x : Signal ℤ) : Signal ℤ := channel (polyphase 2 (by norm_num) x) 1
25 
26 theorem even_apply (x : Signal ℤ) (n : ℤ) : even x n = x (2*n) := by
27   change x ((2:ℤ)*n + 0) = _
28   rw [add_zero]
29 
30 theorem odd_apply (x : Signal ℤ) (n : ℤ) : odd x n = x (2*n+1) := rfl
31 
32 theorem interleaved_energy (x : Signal ℤ) : ‖even x‖ ^ 2 + ‖odd x‖ ^ 2 = ‖x‖ ^ 2 := by
33   have h := channel_energy (polyphase 2 (by norm_num) x)
34   rw [Fin.sum_univ_two, polyphase_energy] at h
35   exact h
36 
37 noncomputable def analysisLow (x : Signal ℤ) : Signal ℤ := low (even x) (odd x)
38 noncomputable def analysisHigh (x : Signal ℤ) : Signal ℤ := high (even x) (odd x)
39 
40 theorem haar_energy (x : Signal ℤ) :
41     ‖x‖ ^ 2 = ‖analysisLow x‖ ^ 2 + ‖analysisHigh x‖ ^ 2 := by
42   rw [analysisLow, analysisHigh, energy, interleaved_energy]
43 
44 theorem haar_low_samples (x : Signal ℤ) (n : ℤ) :
45     analysisLow x n = ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * (x (2*n) + x (2*n+1)) := by
46   rw [analysisLow, low_apply, even_apply, odd_apply]
47 
48 theorem haar_high_samples (x : Signal ℤ) (n : ℤ) :
49     analysisHigh x n = ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * (x (2*n) - x (2*n+1)) := by
50   rw [analysisHigh, high_apply, even_apply, odd_apply]
51 
52 end KomorebiPaperV.HaarChannels

Back to source controls