FiniteTransforms.lean

1 import Mathlib.Analysis.Real.Sqrt
2 import KomorebiPaperV.Lifting
3 import KomorebiPaperV.Packets
4 
5 /-!
6 Author: Komorebi P.
7 Checked source; see the bundled build and axiom audit.
8 Flat even-length indexing, finite lifting, and exactly normalized real Haar pairs.
9 The infinite l2 energy/completeness arguments are not supplied by finite identities.
10 -/
11 
12 open scoped BigOperators
13 namespace KomorebiPaperV.FiniteTransforms
14 
15 variable {K : Type*}
16 
17 /-- Valid even for n=0. This is literal flat-signal indexing, not an assumed address map. -/
18 def flatAddressEquiv (n : ℕ) : Fin (2 * n) ≃ Fin n × Fin 2 where
19   toFun j := (⟨j.val / 2, by have := j.isLt; omega⟩,
20     ⟨j.val % 2, by omega⟩)
21   invFun p := ⟨2 * p.1.val + p.2.val, by
22     have hi := p.1.isLt
23     have hb := p.2.isLt
24     omega⟩
25   left_inv j := by apply Fin.ext; dsimp; omega
26   right_inv p := by
27     apply Prod.ext
28     · apply Fin.ext
29       dsimp
30       have hb := p.2.isLt
31       omega
32     · apply Fin.ext
33       dsimp
34       have hb := p.2.isLt
35       omega
36 
37 def pairChannels {I : Type*} (c : I → Fin 2 → K) : I → K × K :=
38   fun i => (c i 0, c i 1)
39 
40 def unpairChannels {I : Type*} (p : I → K × K) : I → Fin 2 → K :=
41   fun i b => if b = 0 then (p i).1 else (p i).2
42 
43 theorem unpair_pair {I : Type*} (c : I → Fin 2 → K) :
44     unpairChannels (pairChannels c) = c := by
45   funext i b
46   fin_cases b <;> simp [unpairChannels, pairChannels]
47 
48 theorem pair_unpair {I : Type*} (p : I → K × K) :
49     pairChannels (unpairChannels p) = p := by
50   funext i
51   apply Prod.ext <;> simp [unpairChannels, pairChannels]
52 
53 def flatAnalysis (n : ℕ) (x : Fin (2 * n) → K) : Fin n → K × K :=
54   pairChannels (KomorebiPaperV.analyzeAddress (flatAddressEquiv n) x)
55 
56 def flatSynthesis (n : ℕ) (p : Fin n → K × K) : Fin (2 * n) → K :=
57   KomorebiPaperV.synthesizeAddress (flatAddressEquiv n) (unpairChannels p)
58 
59 theorem flat_synthesis_analysis (n : ℕ) (x : Fin (2 * n) → K) :
60     flatSynthesis n (flatAnalysis n x) = x := by
61   rw [flatSynthesis, flatAnalysis, unpair_pair]
62   exact KomorebiPaperV.address_synthesize_analyze (flatAddressEquiv n) x
63 
64 theorem flat_analysis_synthesis (n : ℕ) (p : Fin n → K × K) :
65     flatAnalysis n (flatSynthesis n p) = p := by
66   rw [flatAnalysis, flatSynthesis, KomorebiPaperV.address_analyze_synthesize]
67   exact pair_unpair p
68 
69 section Lifting
70 variable [Field K] [CharZero K]
71 
72 def liftFlat (n : ℕ) (x : Fin (2 * n) → K) : Fin (2 * n) → K :=
73   flatSynthesis n (fun i => KomorebiPaperV.liftingAnalysis (flatAnalysis n x i))
74 
75 def unliftFlat (n : ℕ) (x : Fin (2 * n) → K) : Fin (2 * n) → K :=
76   flatSynthesis n (fun i => KomorebiPaperV.liftingSynthesis (flatAnalysis n x i))
77 
78 theorem unlift_lift_flat (n : ℕ) (x : Fin (2 * n) → K) :
79     unliftFlat n (liftFlat n x) = x := by
80   simp only [unliftFlat, liftFlat, flat_analysis_synthesis,
81     KomorebiPaperV.lifting_synthesis_analysis, flat_synthesis_analysis]
82 
83 theorem lift_unlift_flat (n : ℕ) (x : Fin (2 * n) → K) :
84     liftFlat n (unliftFlat n x) = x := by
85   simp only [liftFlat, unliftFlat, flat_analysis_synthesis,
86     KomorebiPaperV.lifting_analysis_synthesis, flat_synthesis_analysis]
87 end Lifting
88 
89 noncomputable def haar (x : ℝ × ℝ) : ℝ × ℝ :=
90   ((x.1 + x.2) / Real.sqrt 2, (x.1 - x.2) / Real.sqrt 2)
91 
92 theorem haar_involution (x : ℝ × ℝ) : haar (haar x) = x := by
93   have hs : Real.sqrt 2 * Real.sqrt 2 = 2 := by
94     simpa only [pow_two] using (Real.sq_sqrt (show (0 : ℝ) ≤ 2 by norm_num))
95   apply Prod.ext
96   · dsimp [haar]
97     rw [← add_div, div_div, hs]
98     ring
99   · dsimp [haar]
100     rw [← sub_div, div_div, hs]
101     ring
102 
103 theorem haar_pair_energy (x : ℝ × ℝ) :
104     (haar x).1 ^ 2 + (haar x).2 ^ 2 = x.1 ^ 2 + x.2 ^ 2 := by
105   have hs : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
106   dsimp [haar]
107   rw [div_pow, div_pow, hs]
108   ring
109 
110 theorem haar_finite_energy {I : Type*} [Fintype I] (x : I → ℝ × ℝ) :
111     (∑ i, ((haar (x i)).1 ^ 2 + (haar (x i)).2 ^ 2)) =
112       ∑ i, ((x i).1 ^ 2 + (x i).2 ^ 2) := by
113   exact Finset.sum_congr rfl (fun i _ => haar_pair_energy (x i))
114 
115 noncomputable def haarFlat (n : ℕ) (x : Fin (2 * n) → ℝ) : Fin (2 * n) → ℝ :=
116   flatSynthesis n (fun i => haar (flatAnalysis n x i))
117 
118 theorem haar_flat_involution (n : ℕ) (x : Fin (2 * n) → ℝ) :
119     haarFlat n (haarFlat n x) = x := by
120   simp only [haarFlat, flat_analysis_synthesis, haar_involution, flat_synthesis_analysis]
121 
122 section MatrixCriterion
123 variable {I : Type*} [Fintype I] [DecidableEq I] [Semiring K]
124 
125 theorem matrix_eq_of_all_vectors (M D : Matrix I I K)
126     (h : ∀ v : I → K, M.mulVec v = D.mulVec v) : M = D := by
127   classical
128   ext i j
129   have hj := congrFun (h (fun k => if k = j then 1 else 0)) i
130   simpa [Matrix.mulVec, dotProduct, mul_ite] using hj
131 
132 /-- Algebraic matrix criterion. D may be a gain-delay or phase-permutation matrix.
133 The representation of filter-bank operators by those matrices is a separate bridge. -/
134 theorem perfect_reconstruction_matrix_iff (R E D : Matrix I I K) :
135     (∀ v : I → K, (R * E).mulVec v = D.mulVec v) ↔ R * E = D := by
136   constructor
137   · exact matrix_eq_of_all_vectors (R * E) D
138   · intro h v
139     rw [h]
140 end MatrixCriterion
141 
142 end KomorebiPaperV.FiniteTransforms

Back to source controls