WaveletPackets.lean

1 import KomorebiPaperV.HaarChannels
2 import Mathlib.Analysis.InnerProductSpace.Adjoint
3 
4 /-! Author: Komorebi P. Finite-depth literal Haar packet operators and adjoint synthesis. -/
5 namespace KomorebiPaperV.WaveletPackets
6 open KomorebiPaperV.HilbertPackets KomorebiPaperV.HaarChannels
7 abbrev H := Signal ℤ
8 
9 noncomputable def lowLinear : H →ₗ[ℂ] H where
10   toFun := analysisLow
11   map_add' x y := by
12     apply lp.ext
13     funext n
14     simp only [haar_low_samples, lp.coeFn_add, Pi.add_apply]
15     ring
16   map_smul' c x := by
17     apply lp.ext
18     funext n
19     simp only [haar_low_samples, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
20     ring
21 
22 noncomputable def highLinear : H →ₗ[ℂ] H where
23   toFun := analysisHigh
24   map_add' x y := by
25     apply lp.ext
26     funext n
27     simp only [haar_high_samples, lp.coeFn_add, Pi.add_apply]
28     ring
29   map_smul' c x := by
30     apply lp.ext
31     funext n
32     simp only [haar_high_samples, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
33     ring
34 
35 theorem low_norm_bound (x : H) : ‖analysisLow x‖ ≤ ‖x‖ := by
36   have h := haar_energy x
37   nlinarith [sq_nonneg ‖analysisHigh x‖, norm_nonneg x, norm_nonneg (analysisLow x)]
38 
39 theorem high_norm_bound (x : H) : ‖analysisHigh x‖ ≤ ‖x‖ := by
40   have h := haar_energy x
41   nlinarith [sq_nonneg ‖analysisLow x‖, norm_nonneg x, norm_nonneg (analysisHigh x)]
42 
43 noncomputable def lowOp : H →L[ℂ] H := lowLinear.mkContinuous 1 (by
44   intro x
45   simpa [lowLinear] using low_norm_bound x)
46 
47 noncomputable def highOp : H →L[ℂ] H := highLinear.mkContinuous 1 (by
48   intro x
49   simpa [highLinear] using high_norm_bound x)
50 
51 noncomputable def childOp (i : Fin 2) : H →L[ℂ] H := if i = 0 then lowOp else highOp
52 
53 theorem child_energy (x : H) : ∑ i : Fin 2, ‖childOp i x‖ ^ 2 = ‖x‖ ^ 2 := by
54   simpa [Fin.sum_univ_two, childOp, lowOp, lowLinear, highOp, highLinear] using (haar_energy x).symm
55 
56 def Word : ℕ → Type
57   | 0 => Unit
58   | n+1 => Fin 2 × Word n
59 
60 instance wordFintype : (n : ℕ) → Fintype (Word n)
61   | 0 => inferInstanceAs (Fintype Unit)
62   | n+1 => letI := wordFintype n; inferInstanceAs (Fintype (Fin 2 × Word n))
63 
64 noncomputable def packet : (n : ℕ) → Word n → H →L[ℂ] H
65   | 0, _ => ContinuousLinearMap.id ℂ H
66   | n+1, (b,w) => (packet n w).comp (childOp b)
67 
68 theorem packet_energy (n : ℕ) (x : H) : ∑ w : Word n, ‖packet n w x‖ ^ 2 = ‖x‖ ^ 2 := by
69   induction n generalizing x with
70   | zero =>
71     change (∑ w : Unit, ‖x‖ ^ 2) = _
72     simp
73   | succ n ih =>
74     change (∑ w : Fin 2 × Word n, ‖(packet n w.2) (childOp w.1 x)‖ ^ 2) = _
75     rw [Fintype.sum_prod_type]
76     simp_rw [ih]
77     exact child_energy x
78 
79 /-- Complex polarization turns the energy identity into literal adjoint synthesis. -/
80 theorem energy_implies_adjoint_identity {I : Type*} [Fintype I]
81     (W : I → H →L[ℂ] H) (h : ∀ x, ∑ i, ‖W i x‖ ^ 2 = ‖x‖ ^ 2) :
82     (∑ i, (W i).adjoint.comp (W i)) = ContinuousLinearMap.id ℂ H := by
83   have he : (∑ i, (W i).adjoint.comp (W i)).toLinearMap = LinearMap.id := by
84     apply (ext_inner_map _ _).mp
85     intro x
86     change inner ℂ ((∑ i, (W i).adjoint.comp (W i)) x) x = inner ℂ x x
87     simp only [sum_apply, ContinuousLinearMap.comp_apply, sum_inner,
88       ContinuousLinearMap.adjoint_inner_left, inner_self_eq_norm_sq_to_K]
89     exact_mod_cast h x
90   apply ContinuousLinearMap.ext
91   intro x
92   exact LinearMap.congr_fun he x
93 
94 theorem packet_operator_reconstruction (n : ℕ) :
95     (∑ w : Word n, (packet n w).adjoint.comp (packet n w)) = ContinuousLinearMap.id ℂ H :=
96   energy_implies_adjoint_identity (packet n) (packet_energy n)
97 
98 theorem packet_reconstruction (n : ℕ) (x : H) :
99     (∑ w : Word n, (packet n w).adjoint (packet n w x)) = x := by
100   have h := congrArg (fun T : H →L[ℂ] H => T x) (packet_operator_reconstruction n)
101   simpa using h
102 
103 end KomorebiPaperV.WaveletPackets

Back to source controls