ResidueFourierCRT.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.ResidueProjectors
7 
8 /-!
9 # Residue selectors, finite Fourier averages, and CRT coordinates
10 
11 This module proves the Paper II residue-selector algebra over arbitrary
12 semirings, records exact `N → N * k` polyphase refinement, and constructs
13 coprime CRT packet coordinates.  The Fourier realization is deliberately
14 separated from the coefficient selector: it is first derived from an explicit
15 character-orthogonality certificate, and that certificate is then constructed
16 from a primitive root only over a field.  In particular, no primitive-root
17 claim is made for arbitrary rings with zero divisors.
18 -/
19 
20 set_option autoImplicit false
21 
22 namespace Komorebi
23 namespace Residue
24 
25 universe u v
26 
27 /-! ## Residue-projector algebra -/
28 
29 /-- A residue selector is idempotent, over any semiring and module. -/
30 theorem residueProj_idempotent
31     {R : Type u} {A : Type v}
32     [Semiring R] [AddCommMonoid A] [Module R A]
33     (N : Nat) (hN : 0 < N) (r : Fin N) :
34     (residueProj (R := R) (A := A) N hN r).comp
35         (residueProj (R := R) (A := A) N hN r) =
36       residueProj (R := R) (A := A) N hN r := by
37   apply LinearMap.ext
38   intro x
39   exact Packet.fibreProj_idempotent (residueAddress N hN) r x
40 
41 /-- Distinct residue selectors annihilate one another. -/
42 theorem residueProj_orthogonal
43     {R : Type u} {A : Type v}
44     [Semiring R] [AddCommMonoid A] [Module R A]
45     (N : Nat) (hN : 0 < N) {r s : Fin N} (hrs : r ≠ s) :
46     (residueProj (R := R) (A := A) N hN r).comp
47         (residueProj (R := R) (A := A) N hN s) = 0 := by
48   apply LinearMap.ext
49   intro x
50   exact Packet.fibreProj_orthogonal (residueAddress N hN) hrs x
51 
52 /-- The finite family of all residue selectors sums to the identity. -/
53 theorem residueProj_complete
54     {R : Type u} {A : Type v}
55     [Semiring R] [AddCommMonoid A] [Module R A]
56     (N : Nat) (hN : 0 < N) :
57     (∑ r : Fin N, residueProj (R := R) (A := A) N hN r) = LinearMap.id := by
58   apply LinearMap.ext
59   intro x
60   simpa only [LinearMap.sum_apply, LinearMap.id_apply, residueProj_apply] using
61     Packet.fibreProj_reconstruction (residueAddress N hN) x
62 
63 /-- Paper II polyphase refinement from modulus `N` to modulus `N * k`. -/
64 theorem polyphase_refinement
65     {R : Type u} {A : Type v}
66     [Semiring R] [AddCommMonoid A] [Module R A]
67     (N k : Nat) (hN : 0 < N) (hk : 0 < k) (r : Fin N) :
68     residueProj (R := R) (A := A) N hN r =
69       ∑ s : Fin (N * k),
70         if mergeAddress N k hN s = r then
71           residueProj (R := R) (A := A) (N * k) (Nat.mul_pos hN hk) s
72         else 0 :=
73   residueProj_refinement N k hN hk r
74 
75 /-! ## Finite Fourier realization -/
76 
77 /-- The unnormalized coefficientwise Fourier kernel over a commutative semiring.
78 The three scalars are deliberately independent: no inverse or division
79 hypothesis is built into this definition. -/
80 def ringFourierKernel
81     {R : Type u} [CommSemiring R]
82     (N : Nat) (omega omegaDual : R) (j : Fin N) (n : Nat) : R :=
83   ∑ k : Fin N, (omegaDual ^ (j.val * k.val)) * (omega ^ (n * k.val))
84 
85 /-- The finite residue-index version of `ringFourierKernel`.  Unlike the
86 arbitrary-address kernel, both character labels range over the finite type
87 `Fin N`; consequently its orthogonality table is finite data. -/
88 def ringFourierResidueKernel
89     {R : Type u} [CommSemiring R]
90     (N : Nat) (omega omegaDual : R) (j r : Fin N) : R :=
91   ∑ k : Fin N, (omegaDual ^ (j.val * k.val)) * (omega ^ (r.val * k.val))
92 
93 /-- If `omega` is an `N`-th root of unity, the arbitrary-address kernel is
94 periodic in its coefficient address and is therefore determined by the
95 finite residue-index kernel. -/
96 theorem ringFourierKernel_eq_residueKernel
97     {R : Type u} [CommSemiring R]
98     (N : Nat) (hN : 0 < N) (omega omegaDual : R)
99     (homega : omega ^ N = 1) (j : Fin N) (n : Nat) :
100     ringFourierKernel N omega omegaDual j n =
101       ringFourierResidueKernel N omega omegaDual j
102         ⟨n % N, Nat.mod_lt n hN⟩ := by
103   apply Finset.sum_congr rfl
104   intro k _hk
105   congr 1
106   calc
107     omega ^ (n * k.val) = (omega ^ n) ^ k.val := by rw [pow_mul]
108     _ = (omega ^ (n % N)) ^ k.val := by rw [pow_eq_pow_mod n homega]
109     _ = omega ^ ((n % N) * k.val) := by rw [pow_mul]
110 
111 /-- A genuinely finite general-ring Fourier certificate.  Its character
112 orthogonality premise is a finite `N × N` table; `omega_pow_order` is then
113 used to extend that table periodically to every coefficient address. -/
114 structure FiniteRingFourierOrthogonalityCertificate
115     (R : Type u) [CommSemiring R] (N : Nat)
116     (omega omegaDual eta : R) : Prop where
117   omega_pow_order : omega ^ N = 1
118   weighted_residue_sum_eq (j r : Fin N) :
119     eta * ringFourierResidueKernel N omega omegaDual j r =
120       if r = j then 1 else 0
121 
122 /-- The legacy coefficientwise orthogonality certificate used in Paper II.
123 It is meaningful over an arbitrary commutative semiring, including rings with
124 zero divisors, and assumes neither division by `N` nor that `omegaDual` is an
125 inverse of `omega`.  New proofs should generally use the finite certificate
126 above and derive this interface through `toRingCertificate`. -/
127 structure RingFourierOrthogonalityCertificate
128     (R : Type u) [CommSemiring R] (N : Nat)
129     (omega omegaDual eta : R) : Prop where
130   weighted_sum_eq (j : Fin N) (n : Nat) :
131     eta * ringFourierKernel N omega omegaDual j n =
132       if n % N = j.val then 1 else 0
133 
134 /-- A finite residue-index certificate supplies the legacy arbitrary-address
135 certificate by periodic reduction.  This theorem is the substantive bridge
136 which removes the former infinite family of certificate obligations. -/
137 theorem FiniteRingFourierOrthogonalityCertificate.toRingCertificate
138     {R : Type u} [CommSemiring R]
139     (N : Nat) (hN : 0 < N) (omega omegaDual eta : R)
140     (certificate :
141       FiniteRingFourierOrthogonalityCertificate R N omega omegaDual eta) :
142     RingFourierOrthogonalityCertificate R N omega omegaDual eta := by
143   refine ⟨?_⟩
144   intro j n
145   rw [ringFourierKernel_eq_residueKernel N hN omega omegaDual
146     certificate.omega_pow_order j n]
147   rw [certificate.weighted_residue_sum_eq]
148   congr 1
149   simp only [Fin.ext_iff]
150 
151 /-- The division-free coefficientwise Fourier average attached to independent
152 scalars `omega`, `omegaDual`, and `eta`.  It is the diagonal action of
153 `eta ∑ₖ (omegaDual)^(j k) U^k` on coefficient sequences. -/
154 def ringFourierAverage
155     {R : Type u} {A : Type v}
156     [CommSemiring R] [AddCommMonoid A] [Module R A]
157     (N : Nat) (omega omegaDual eta : R) (j : Fin N) :
158     Module.End R (Nat → A) where
159   toFun x n := (eta * ringFourierKernel N omega omegaDual j n) • x n
160   map_add' x y := by
161     funext n
162     exact smul_add _ _ _
163   map_smul' c x := by
164     funext n
165     simp only [Pi.smul_apply, smul_smul, RingHom.id_apply]
166     rw [mul_comm]
167 
168 @[simp] theorem ringFourierAverage_apply
169     {R : Type u} {A : Type v}
170     [CommSemiring R] [AddCommMonoid A] [Module R A]
171     (N : Nat) (omega omegaDual eta : R) (j : Fin N)
172     (x : Nat → A) (n : Nat) :
173     ringFourierAverage (A := A) N omega omegaDual eta j x n =
174       (eta * ringFourierKernel N omega omegaDual j n) • x n :=
175   rfl
176 
177 /-- An explicit coefficientwise orthogonality certificate identifies the
178 division-free Fourier average with the residue selector over any commutative
179 semiring. -/
180 theorem ringFourierAverage_eq_residueProj_of_certificate
181     {R : Type u} {A : Type v}
182     [CommSemiring R] [AddCommMonoid A] [Module R A]
183     (N : Nat) (hN : 0 < N) (omega omegaDual eta : R)
184     (certificate :
185       RingFourierOrthogonalityCertificate R N omega omegaDual eta)
186     (j : Fin N) :
187     ringFourierAverage (A := A) N omega omegaDual eta j =
188       residueProj (R := R) (A := A) N hN j := by
189   apply LinearMap.ext
190   intro x
191   funext n
192   rw [ringFourierAverage_apply, certificate.weighted_sum_eq]
193   change
194     (if n % N = j.val then (1 : R) else 0) • x n =
195       if residueAddress N hN n = j then x n else 0
196   by_cases h : n % N = j.val
197   · have haddress : residueAddress N hN n = j := Fin.ext h
198     simp [h, haddress]
199   · have haddress : residueAddress N hN n ≠ j := by
200       intro heq
201       exact h (congrArg Fin.val heq)
202     simp [h, haddress]
203 
204 /-- The division-free Fourier average equals the residue selector from only
205 a finite residue-index orthogonality table and the root-periodicity datum. -/
206 theorem ringFourierAverage_eq_residueProj_of_finite_certificate
207     {R : Type u} {A : Type v}
208     [CommSemiring R] [AddCommMonoid A] [Module R A]
209     (N : Nat) (hN : 0 < N) (omega omegaDual eta : R)
210     (certificate :
211       FiniteRingFourierOrthogonalityCertificate R N omega omegaDual eta)
212     (j : Fin N) :
213     ringFourierAverage (A := A) N omega omegaDual eta j =
214       residueProj (R := R) (A := A) N hN j :=
215   ringFourierAverage_eq_residueProj_of_certificate N hN omega omegaDual eta
216     (certificate.toRingCertificate N hN omega omegaDual eta) j
217 
218 /-- The scalar character sum acting on coefficient address `n` in the
219 `j`-th finite Fourier average.  Reducing `n` modulo `N` is harmless for a
220 primitive `N`-th root and makes the exact orthogonality statement explicit. -/
221 def fourierKernel
222     {K : Type u} [Field K]
223     (N : Nat) (omega : K) (j : Fin N) (n : Nat) : K :=
224   ∑ k : Fin N, ((omega ^ (n % N)) / (omega ^ j.val)) ^ k.val
225 
226 /-- An explicit finite-character orthogonality certificate.  Besides the
227 character-sum identity, it records the nonvanishing of the group order needed
228 to normalize the average. -/
229 structure FourierOrthogonalityCertificate
230     (K : Type u) [Field K] (N : Nat) (omega : K) : Prop where
231   order_ne_zero : (N : K) ≠ 0
232   sum_eq (j : Fin N) (n : Nat) :
233     fourierKernel N omega j n =
234       if n % N = j.val then (N : K) else 0
235 
236 /-- The coefficientwise finite Fourier average.  Its multiplier is exactly
237 `N⁻¹ ∑ₖ (omega^(n mod N) / omega^j)^k`, the eigenvalue of the operator
238 average `N⁻¹ ∑ₖ omega^(-jk) U^k` at coefficient address `n`. -/
239 def fourierAverage
240     {K : Type u} {A : Type v}
241     [Field K] [AddCommMonoid A] [Module K A]
242     (N : Nat) (omega : K) (j : Fin N) : Module.End K (Nat → A) where
243   toFun x n := ((N : K)⁻¹ * fourierKernel N omega j n) • x n
244   map_add' x y := by
245     funext n
246     exact smul_add _ _ _
247   map_smul' c x := by
248     funext n
249     simp only [Pi.smul_apply, smul_smul, RingHom.id_apply]
250     rw [mul_comm]
251 
252 @[simp] theorem fourierAverage_apply
253     {K : Type u} {A : Type v}
254     [Field K] [AddCommMonoid A] [Module K A]
255     (N : Nat) (omega : K) (j : Fin N) (x : Nat → A) (n : Nat) :
256     fourierAverage (A := A) N omega j x n =
257       ((N : K)⁻¹ * fourierKernel N omega j n) • x n :=
258   rfl
259 
260 /-- An explicit orthogonality certificate identifies the finite Fourier
261 average with the coefficient residue selector. -/
262 theorem fourierAverage_eq_residueProj_of_certificate
263     {K : Type u} {A : Type v}
264     [Field K] [AddCommMonoid A] [Module K A]
265     (N : Nat) (hN : 0 < N) (omega : K)
266     (certificate : FourierOrthogonalityCertificate K N omega)
267     (j : Fin N) :
268     fourierAverage (A := A) N omega j =
269       residueProj (R := K) (A := A) N hN j := by
270   apply LinearMap.ext
271   intro x
272   funext n
273   rw [fourierAverage_apply, certificate.sum_eq]
274   change
275     ((N : K)⁻¹ * (if n % N = j.val then (N : K) else 0)) • x n =
276       if residueAddress N hN n = j then x n else 0
277   by_cases h : n % N = j.val
278   · have haddress : residueAddress N hN n = j := Fin.ext h
279     simp [h, haddress, certificate.order_ne_zero]
280   · have haddress : residueAddress N hN n ≠ j := by
281       intro heq
282       exact h (congrArg Fin.val heq)
283     simp [h, haddress]
284 
285 /-- Over a field, a primitive `N`-th root supplies the exact character
286 orthogonality certificate.  This is intentionally not stated over an
287 arbitrary zero-divisor ring. -/
288 theorem primitiveRoot_fourierOrthogonalityCertificate
289     {K : Type u} [Field K]
290     (N : Nat) (hN : 0 < N) (omega : K)
291     (homega : IsPrimitiveRoot omega N) :
292     FourierOrthogonalityCertificate K N omega := by
293   let _ : NeZero N := ⟨Nat.ne_of_gt hN⟩
294   have homega0 : omega ≠ 0 := homega.ne_zero (Nat.ne_of_gt hN)
295   refine
296     { order_ne_zero := (homega.neZero' : NeZero (N : K)).out
297       sum_eq := ?_ }
298   intro j n
299   by_cases hnj : n % N = j.val
300   · simp [fourierKernel, hnj, homega0]
301   · rw [ite_eq_right hnj]
302     let q : K := (omega ^ (n % N)) / (omega ^ j.val)
303     have hpowers : omega ^ (n % N) ≠ omega ^ j.val := by
304       intro heq
305       exact hnj (homega.pow_inj (Nat.mod_lt n hN) j.isLt heq)
306     have hq_ne_one : q ≠ 1 := by
307       intro hq
308       exact hpowers ((div_eq_one_iff_eq (pow_ne_zero _ homega0)).mp hq)
309     have hq_pow : q ^ N = 1 := by
310       dsimp only [q]
311       rw [div_pow]
312       have hnum : (omega ^ (n % N)) ^ N = 1 := by
313         rw [← pow_mul, Nat.mul_comm, pow_mul, homega.pow_eq_one, one_pow]
314       have hden : (omega ^ j.val) ^ N = 1 := by
315         rw [← pow_mul, Nat.mul_comm, pow_mul, homega.pow_eq_one, one_pow]
316       rw [hnum, hden, div_one]
317     change ∑ k : Fin N, q ^ k.val = 0
318     rw [Fin.sum_univ_eq_sum_range, geom_sum_eq hq_ne_one, hq_pow]
319     simp
320 
321 /-- Root-of-unity realization of a residue selector over a field. -/
322 theorem fourierAverage_eq_residueProj_of_primitiveRoot
323     {K : Type u} {A : Type v}
324     [Field K] [AddCommMonoid A] [Module K A]
325     (N : Nat) (hN : 0 < N) (omega : K)
326     (homega : IsPrimitiveRoot omega N) (j : Fin N) :
327     fourierAverage (A := A) N omega j =
328       residueProj (R := K) (A := A) N hN j :=
329   fourierAverage_eq_residueProj_of_certificate N hN omega
330     (primitiveRoot_fourierOrthogonalityCertificate N hN omega homega) j
331 
332 /-! ## Coprime CRT coordinates and product selectors -/
333 
334 /-- The two residue components of a residue modulo `m * n`. -/
335 def crtComponents
336     (m n : Nat) (hm : 0 < m) (hn : 0 < n) :
337     Fin (m * n) → Fin m × Fin n :=
338   fun s =>
339     (⟨s.val % m, Nat.mod_lt _ hm⟩,
340       ⟨s.val % n, Nat.mod_lt _ hn⟩)
341 
342 /-- The coprime Chinese-remainder bijection on finite residue labels. -/
343 def crtEquiv
344     (m n : Nat) (hm : 0 < m) (hn : 0 < n)
345     (hcoprime : m.Coprime n) : Fin (m * n) ≃ Fin m × Fin n where
346   toFun := crtComponents m n hm hn
347   invFun p :=
348     ⟨(Nat.chineseRemainder hcoprime p.1.val p.2.val).val,
349       Nat.chineseRemainder_lt_mul hcoprime p.1.val p.2.val
350         (Nat.ne_of_gt hm) (Nat.ne_of_gt hn)⟩
351   left_inv s := by
352     apply Fin.ext
353     let c := Nat.chineseRemainder hcoprime (s.val % m) (s.val % n)
354     have hs_mod : s.val ≡ c.val [MOD m * n] :=
355       Nat.chineseRemainder_modEq_unique hcoprime
356         (Nat.mod_modEq s.val m).symm (Nat.mod_modEq s.val n).symm
357     change c.val = s.val
358     calc
359       c.val = c.val % (m * n) :=
360         (Nat.mod_eq_of_lt
361           (Nat.chineseRemainder_lt_mul hcoprime (s.val % m) (s.val % n)
362             (Nat.ne_of_gt hm) (Nat.ne_of_gt hn))).symm
363       _ = s.val % (m * n) := hs_mod.symm
364       _ = s.val := Nat.mod_eq_of_lt s.isLt
365   right_inv p := by
366     apply Prod.ext
367     · apply Fin.ext
368       exact Nat.mod_eq_of_modEq
369         (Nat.chineseRemainder hcoprime p.1.val p.2.val).property.1 p.1.isLt
370     · apply Fin.ext
371       exact Nat.mod_eq_of_modEq
372         (Nat.chineseRemainder hcoprime p.1.val p.2.val).property.2 p.2.isLt
373 
374 /-- The component map itself is bijective for positive coprime moduli. -/
375 theorem crtComponents_bijective
376     (m n : Nat) (hm : 0 < m) (hn : 0 < n)
377     (hcoprime : m.Coprime n) :
378     Function.Bijective (crtComponents m n hm hn) :=
379   (crtEquiv m n hm hn hcoprime).bijective
380 
381 /-- Reducing an address modulo `m * n` and taking its CRT components agrees
382 with reducing the address directly modulo `m` and modulo `n`. -/
383 theorem crtComponents_residueAddress
384     (m n : Nat) (hm : 0 < m) (hn : 0 < n) (a : Nat) :
385     crtComponents m n hm hn
386         (residueAddress (m * n) (Nat.mul_pos hm hn) a) =
387       (residueAddress m hm a, residueAddress n hn a) := by
388   apply Prod.ext
389   · apply Fin.ext
390     exact Nat.mod_mod_of_dvd a ⟨n, rfl⟩
391   · apply Fin.ext
392     exact Nat.mod_mod_of_dvd a ⟨m, Nat.mul_comm m n⟩
393 
394 /-- Equality of a composite residue address is equivalent to equality of its
395 two coprime component addresses. -/
396 theorem residueAddress_eq_iff_crtComponents
397     (m n : Nat) (hm : 0 < m) (hn : 0 < n)
398     (hcoprime : m.Coprime n) (a : Nat) (s : Fin (m * n)) :
399     residueAddress (m * n) (Nat.mul_pos hm hn) a = s ↔
400       residueAddress m hm a = (crtComponents m n hm hn s).1 ∧
401       residueAddress n hn a = (crtComponents m n hm hn s).2 := by
402   constructor
403   · intro has
404     have hcomponents := congrArg (crtComponents m n hm hn) has
405     rw [crtComponents_residueAddress] at hcomponents
406     exact Prod.ext_iff.mp hcomponents
407   · rintro ⟨hmcomp, hncomp⟩
408     apply (crtEquiv m n hm hn hcoprime).injective
409     change
410       crtComponents m n hm hn
411           (residueAddress (m * n) (Nat.mul_pos hm hn) a) =
412         crtComponents m n hm hn s
413     rw [crtComponents_residueAddress]
414     exact Prod.ext hmcomp hncomp
415 
416 /-- A composite residue selector is the product of its two coprime component
417 selectors, with the `m`-selector applied last. -/
418 theorem residueProj_crt
419     {R : Type u} {A : Type v}
420     [Semiring R] [AddCommMonoid A] [Module R A]
421     (m n : Nat) (hm : 0 < m) (hn : 0 < n)
422     (hcoprime : m.Coprime n) (s : Fin (m * n)) :
423     (residueProj (R := R) (A := A) m hm (crtComponents m n hm hn s).1).comp
424         (residueProj (R := R) (A := A) n hn (crtComponents m n hm hn s).2) =
425       residueProj (R := R) (A := A) (m * n) (Nat.mul_pos hm hn) s := by
426   apply LinearMap.ext
427   intro x
428   funext a
429   simp only [LinearMap.comp_apply, residueProj_apply, Packet.fibreProj]
430   by_cases hma : residueAddress m hm a = (crtComponents m n hm hn s).1 <;>
431     by_cases hna : residueAddress n hn a = (crtComponents m n hm hn s).2 <;>
432     simp [hma, hna,
433       residueAddress_eq_iff_crtComponents m n hm hn hcoprime a s]
434 
435 /-- The two coprime component selectors commute, and their reverse product is
436 the same composite residue selector. -/
437 theorem residueProj_crt_comm
438     {R : Type u} {A : Type v}
439     [Semiring R] [AddCommMonoid A] [Module R A]
440     (m n : Nat) (hm : 0 < m) (hn : 0 < n)
441     (hcoprime : m.Coprime n) (s : Fin (m * n)) :
442     (residueProj (R := R) (A := A) n hn (crtComponents m n hm hn s).2).comp
443         (residueProj (R := R) (A := A) m hm (crtComponents m n hm hn s).1) =
444       residueProj (R := R) (A := A) (m * n) (Nat.mul_pos hm hn) s := by
445   apply LinearMap.ext
446   intro x
447   funext a
448   simp only [LinearMap.comp_apply, residueProj_apply, Packet.fibreProj]
449   by_cases hma : residueAddress m hm a = (crtComponents m n hm hn s).1 <;>
450     by_cases hna : residueAddress n hn a = (crtComponents m n hm hn s).2 <;>
451     simp [hma, hna,
452       residueAddress_eq_iff_crtComponents m n hm hn hcoprime a s]
453 
454 /-! ## Dyadic--odd specialization -/
455 
456 /-- An odd modulus is coprime to every dyadic power. -/
457 theorem twoPow_coprime_of_odd
458     (a M : Nat) (hodd : Odd M) : (2 ^ a).Coprime M := by
459   exact hodd.coprime_two_left.pow_left a
460 
461 /-- CRT identifies residues modulo `2^a * M` with dyadic and odd residue
462 labels whenever `M` is positive and odd. -/
463 def dyadicOddEquiv
464     (a M : Nat) (hM : 0 < M) (hodd : Odd M) :
465     Fin (2 ^ a * M) ≃ Fin (2 ^ a) × Fin M :=
466   crtEquiv (2 ^ a) M (pow_pos (by decide) a) hM
467     (twoPow_coprime_of_odd a M hodd)
468 
469 /-- The dyadic--odd component map is a bijection. -/
470 theorem dyadicOddComponents_bijective
471     (a M : Nat) (hM : 0 < M) (hodd : Odd M) :
472     Function.Bijective
473       (crtComponents (2 ^ a) M (pow_pos (by decide) a) hM) :=
474   (dyadicOddEquiv a M hM hodd).bijective
475 
476 /-- Dyadic--odd packet factorization, in both composition orders. -/
477 theorem residueProj_dyadicOdd
478     {R : Type u} {A : Type v}
479     [Semiring R] [AddCommMonoid A] [Module R A]
480     (a M : Nat) (hM : 0 < M) (hodd : Odd M) (s : Fin (2 ^ a * M)) :
481     let h2 : 0 < 2 ^ a := pow_pos (by decide) a
482     let components := crtComponents (2 ^ a) M h2 hM s
483     residueProj (R := R) (A := A) (2 ^ a * M) (Nat.mul_pos h2 hM) s =
484         (residueProj (R := R) (A := A) (2 ^ a) h2 components.1).comp
485           (residueProj (R := R) (A := A) M hM components.2) ∧
486       residueProj (R := R) (A := A) (2 ^ a * M) (Nat.mul_pos h2 hM) s =
487         (residueProj (R := R) (A := A) M hM components.2).comp
488           (residueProj (R := R) (A := A) (2 ^ a) h2 components.1) := by
489   dsimp only
490   let h2 : 0 < 2 ^ a := pow_pos (by decide) a
491   let hcoprime : (2 ^ a).Coprime M := twoPow_coprime_of_odd a M hodd
492   constructor
493   · exact (residueProj_crt (R := R) (A := A)
494       (2 ^ a) M h2 hM hcoprime s).symm
495   · exact (residueProj_crt_comm (R := R) (A := A)
496       (2 ^ a) M h2 hM hcoprime s).symm
497 
498 #print axioms residueProj_idempotent
499 #print axioms residueProj_orthogonal
500 #print axioms residueProj_complete
501 #print axioms polyphase_refinement
502 #print axioms ringFourierKernel_eq_residueKernel
503 #print axioms FiniteRingFourierOrthogonalityCertificate.toRingCertificate
504 #print axioms ringFourierAverage_eq_residueProj_of_certificate
505 #print axioms ringFourierAverage_eq_residueProj_of_finite_certificate
506 #print axioms fourierAverage_eq_residueProj_of_certificate
507 #print axioms primitiveRoot_fourierOrthogonalityCertificate
508 #print axioms fourierAverage_eq_residueProj_of_primitiveRoot
509 #print axioms crtEquiv
510 #print axioms crtComponents_bijective
511 #print axioms residueProj_crt
512 #print axioms residueProj_crt_comm
513 #print axioms dyadicOddComponents_bijective
514 #print axioms residueProj_dyadicOdd
515 
516 end Residue
517 end Komorebi

Back to source controls