WalshTransform.lean

1 module
2 public import StructuredTensor
3 public import Mathlib.LinearAlgebra.Matrix.Block
4 public import Mathlib.Data.Nat.Log
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII 4.7: recursively constructed Walsh matrices, actual butterfly
10 application, and an exact count of scalar additions/subtractions.
11 -/
12 @[expose] public section
13 set_option autoImplicit false
14 namespace KomorebiPaperVIII
15 open Matrix
16 open scoped BigOperators Kronecker
17 
18 /-- The first tensor coordinate distinguishes the upper and lower half. -/
19 def walshTwo : Matrix (Fin 2) (Fin 2) ℂ := !![1,1;1,-1]
20 
21 theorem walsh_two_orthogonal : walshTwo * walshTwoᵀ = (2:ℂ) • 1 := by
22   ext i j
23   fin_cases i <;> fin_cases j <;> norm_num [walshTwo, Matrix.mul_apply, Fin.sum_univ_two]
24 
25 def walshMatrix : (k : ℕ) → Matrix (TensorIndex 2 k) (TensorIndex 2 k) ℂ
26   | 0 => fun _ _ => 1
27   | k+1 => walshTwo ⊗ₖ walshMatrix k
28 
29 theorem walsh_recursion (k : ℕ) :
30     walshMatrix (k+1) = walshTwo ⊗ₖ walshMatrix k := rfl
31 
32 /-- This is the ordinary transpose identity over the complex scalar field. -/
33 theorem walsh_orthogonal (k : ℕ) :
34     walshMatrix k * (walshMatrix k)ᵀ = ((2:ℂ)^k) • 1 := by
35   induction k with
36   | zero =>
37     have hb : walshMatrix 0 = 1 := by
38       ext i j
39       cases i
40       cases j
41       change (1:ℂ) = if (PUnit.unit : Unit) = PUnit.unit then 1 else 0
42       simp
43     rw [hb]
44     simp
45   | succ k ih =>
46     change (walshTwo ⊗ₖ walshMatrix k) * (walshTwo ⊗ₖ walshMatrix k)ᵀ = _
47     rw [← Matrix.kroneckerMap_transpose, ← Matrix.mul_kronecker_mul, walsh_two_orthogonal, ih,
48       Matrix.smul_kronecker, Matrix.kronecker_smul, Matrix.one_kronecker_one, smul_smul]
49     change ((2:ℂ) * 2^k) • (1 : Matrix (Fin 2 × TensorIndex 2 k) (Fin 2 × TensorIndex 2 k) ℂ) =
50       (2:ℂ)^(k+1) • (1 : Matrix (Fin 2 × TensorIndex 2 k) (Fin 2 × TensorIndex 2 k) ℂ)
51     rw [pow_succ, mul_comm]
52 
53 /-- Two recursive transforms of the elementwise sum and difference of the halves. -/
54 def walshApply : (k : ℕ) → (TensorIndex 2 k → ℂ) → (TensorIndex 2 k → ℂ)
55   | 0, x => x
56   | k+1, x => fun p =>
57       if p.1 = 0 then walshApply k (fun u => x (0,u)+x (1,u)) p.2
58       else walshApply k (fun u => x (0,u)-x (1,u)) p.2
59 
60 theorem walsh_apply_correct (k : ℕ) (x : TensorIndex 2 k → ℂ) :
61     walshApply k x = walshMatrix k *ᵥ x := by
62   induction k with
63   | zero =>
64     funext i
65     cases i
66     change x PUnit.unit = ∑ i : Unit, (1:ℂ)*x i
67     simp only [one_mul]
68     symm
69     apply Finset.sum_eq_single PUnit.unit
70     · intro b _ h
71       cases b
72       exact (h rfl).elim
73     · intro h
74       exact (h (Finset.mem_univ _)).elim
75   | succ k ih =>
76     funext p
77     rcases p with ⟨i,u⟩
78     change (if i = 0 then walshApply k (fun v => x (0,v)+x (1,v)) u
79       else walshApply k (fun v => x (0,v)-x (1,v)) u) =
80         ∑ v : Fin 2 × TensorIndex 2 k, (walshTwo i v.1 * walshMatrix k u v.2) * x v
81     simp_rw [ih]
82     fin_cases i <;>
83       simp [walshTwo, Matrix.mulVec, dotProduct, Fintype.sum_prod_type,
84         Fin.sum_univ_two, mul_add, Finset.sum_add_distrib, sub_eq_add_neg]
85 
86 /-- Addition/subtraction event addresses of the actual recursive algorithm. -/
87 def WalshOperation : ℕ → Type
88   | 0 => Empty
89   | k+1 => (Fin 2 × WalshOperation k) ⊕ (TensorIndex 2 k × Bool)
90 
91 instance walshOperationFintype (k : ℕ) : Fintype (WalshOperation k) := by
92   induction k with
93   | zero => exact inferInstanceAs (Fintype Empty)
94   | succ k ih =>
95     change Fintype ((Fin 2 × WalshOperation k) ⊕ (TensorIndex 2 k × Bool))
96     letI := ih
97     exact inferInstance
98 
99 theorem walsh_operation_count (k : ℕ) : Fintype.card (WalshOperation k) = k*2^k := by
100   induction k with
101   | zero =>
102     change Fintype.card Empty = _
103     simp
104   | succ k ih =>
105     change Fintype.card ((Fin 2 × WalshOperation k) ⊕ (TensorIndex 2 k × Bool)) = _
106     simp only [Fintype.card_sum, Fintype.card_prod, Fintype.card_fin, Fintype.card_bool,
107       tensor_dimension, ih, pow_succ]
108     ring
109 
110 theorem walsh_inverse_action (k : ℕ) (x : TensorIndex 2 k → ℂ) :
111     walshMatrix k *ᵥ ((walshMatrix k)ᵀ *ᵥ x) = ((2:ℂ)^k) • x := by
112   rw [Matrix.mulVec_mulVec, walsh_orthogonal, Matrix.smul_mulVec, Matrix.one_mulVec]
113 
114 /-- The manuscript's N log2(N) formula, with N = 2^k. -/
115 theorem walsh_log_operation_count (k : ℕ) :
116     Fintype.card (WalshOperation k) = 2^k * Nat.log2 (2^k) := by
117   rw [walsh_operation_count, Nat.log2_eq_log_two, Nat.log_pow Nat.one_lt_two, mul_comm]
118 
119 end KomorebiPaperVIII
120 
121 -- FINAL AXIOM AUDITS
122 #print axioms KomorebiPaperVIII.walsh_two_orthogonal
123 #print axioms KomorebiPaperVIII.walsh_recursion
124 #print axioms KomorebiPaperVIII.walsh_orthogonal
125 #print axioms KomorebiPaperVIII.walsh_apply_correct
126 #print axioms KomorebiPaperVIII.walsh_operation_count
127 #print axioms KomorebiPaperVIII.walsh_inverse_action
128 
129 #print axioms KomorebiPaperVIII.walsh_log_operation_count
130 
131 #print axioms KomorebiPaperVIII.walshMatrix
132 
133 #print axioms KomorebiPaperVIII.walshApply

Back to source controls