ReleaseCoordinatesFourier.lean

1 import KomorebiVerification.PaperII.ReleaseCoordinatesResidue
2 
3 /-!
4 The literal operator F(X) ↦ F(ωX), its iterates, and its finite weighted
5 average on actual formal power series. These connect the independently
6 proved coefficient-kernel certificate to the printed operator equality.
7 -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace Komorebi.Residue
11 universe u
12 variable {R : Type u}
13 
14 /-- The actual formal substitution F(X) ↦ F(ωX), as an R-linear map. -/
15 def seriesPhase [CommSemiring R] (omega : R) : Module.End R (PowerSeries R) where
16   toFun := PowerSeries.rescale omega
17   map_add' := (PowerSeries.rescale omega).map_add
18   map_smul' c f := by
19     ext n
20     simp only [PowerSeries.coeff_rescale, PowerSeries.coeff_smul, smul_eq_mul,
21       RingHom.id_apply]
22     ring
23 
24 @[simp] theorem seriesPhase_coeff [CommSemiring R]
25     (omega : R) (f : PowerSeries R) (n : Nat) :
26     PowerSeries.coeff n (seriesPhase omega f) = omega ^ n * PowerSeries.coeff n f :=
27   PowerSeries.coeff_rescale f omega n
28 
29 /-- The kth power is the kth iterate of the actual phase operator. -/
30 theorem seriesPhase_pow_coeff [CommSemiring R]
31     (omega : R) (k : Nat) (f : PowerSeries R) (n : Nat) :
32     PowerSeries.coeff n ((seriesPhase omega ^ k) f) =
33       omega ^ (n * k) * PowerSeries.coeff n f := by
34   induction k with
35   | zero => simp
36   | succ k ih =>
37       rw [pow_succ', Module.End.mul_apply, seriesPhase_coeff, ih]
38       rw [Nat.mul_succ, pow_add]
39       ring
40 
41 /-- The Nth operator power is the identity when the phase has order dividing N. -/
42 theorem seriesPhase_pow_order [CommSemiring R]
43     (N : Nat) (omega : R) (h : omega ^ N = 1) :
44     seriesPhase omega ^ N = 1 := by
45   ext f n
46   rw [seriesPhase_pow_coeff, Nat.mul_comm n N, pow_mul, h]
47   simp
48 
49 /-- The finite operator sum appearing in the general-ring theorem. -/
50 def seriesFourierAverage [CommSemiring R]
51     (N : Nat) (omega omegaDual eta : R) (j : Fin N) : Module.End R (PowerSeries R) :=
52   eta • ∑ k : Fin N, (omegaDual ^ (j.val * k.val)) • (seriesPhase omega ^ k.val)
53 
54 /-- Direct evaluation of the finite operator sum gives the independently defined kernel. -/
55 theorem seriesFourierAverage_coeff [CommSemiring R]
56     (N : Nat) (omega omegaDual eta : R) (j : Fin N) (f : PowerSeries R) (n : Nat) :
57     PowerSeries.coeff n (seriesFourierAverage N omega omegaDual eta j f) =
58       (eta * ringFourierKernel N omega omegaDual j n) * PowerSeries.coeff n f := by
59   simp only [seriesFourierAverage, LinearMap.smul_apply, LinearMap.sum_apply,
60     map_smul, map_sum, seriesPhase_pow_coeff, smul_eq_mul,
61     ringFourierKernel]
62   rw [mul_assoc, Finset.sum_mul]
63   congr 1
64   apply Finset.sum_congr rfl
65   intro k _
66   rw [mul_assoc]
67 
68 /-- A finite certificate proves the literal formal-series operator equality. -/
69 theorem seriesFourierAverage_eq_residueProj [CommSemiring R]
70     (N : Nat) (hN : 0 < N) (omega omegaDual eta : R)
71     (h : FiniteRingFourierOrthogonalityCertificate R N omega omegaDual eta) (j : Fin N) :
72     seriesFourierAverage N omega omegaDual eta j = seriesResidueProj N hN j := by
73   ext f n
74   rw [seriesFourierAverage_coeff,
75     (h.toRingCertificate N hN omega omegaDual eta).weighted_sum_eq,
76     seriesResidueProj_coeff]
77   have heq : residueAddress N hN n = j ↔ n % N = j.val := Fin.ext_iff
78   by_cases hn : n % N = j.val
79   · simp [hn, heq.mpr hn]
80   · have hn' : residueAddress N hN n ≠ j := fun h => hn (heq.mp h)
81     simp [hn, hn']
82 
83 /-- Under root periodicity, the field ratio kernel and inverse-power kernel agree. -/
84 theorem ringFourierKernel_inv_eq_fourierKernel [Field R]
85     (N : Nat) (omega : R) (homega : omega ^ N = 1) (j : Fin N) (n : Nat) :
86     ringFourierKernel N omega omega⁻¹ j n = fourierKernel N omega j n := by
87   unfold ringFourierKernel fourierKernel
88   apply Finset.sum_congr rfl
89   intro k _
90   simp only [pow_mul, inv_pow, div_eq_mul_inv, mul_pow]
91   rw [pow_eq_pow_mod n homega]
92   ring
93 
94 /-- A primitive root over a field supplies the manuscript finite ring certificate itself. -/
95 theorem primitiveRoot_finiteRingFourierCertificate [Field R]
96     (N : Nat) (hN : 0 < N) (omega : R) (homega : IsPrimitiveRoot omega N) :
97     FiniteRingFourierOrthogonalityCertificate R N omega omega⁻¹ (N : R)⁻¹ := by
98   refine ⟨homega.pow_eq_one, ?_⟩
99   intro j r
100   have hc := primitiveRoot_fourierOrthogonalityCertificate N hN omega homega
101   have hker : ringFourierResidueKernel N omega omega⁻¹ j r =
102       fourierKernel N omega j r.val :=
103     ringFourierKernel_inv_eq_fourierKernel N omega homega.pow_eq_one j r.val
104   rw [hker, hc.sum_eq, Nat.mod_eq_of_lt r.isLt]
105   by_cases hr : r = j
106   · subst r
107     simp [hc.order_ne_zero]
108   · have hv : r.val ≠ j.val := fun h => hr (Fin.ext h)
109     simp [hr, hv]
110 
111 /-- Character realization as a finite sum of powers of actual series substitution. -/
112 theorem seriesFourierAverage_eq_residueProj_of_primitiveRoot [Field R]
113     (N : Nat) (hN : 0 < N) (omega : R) (homega : IsPrimitiveRoot omega N) (j : Fin N) :
114     (N : R)⁻¹ • (∑ k : Fin N, (omega⁻¹ ^ (j.val * k.val)) •
115       (seriesPhase omega ^ k.val)) = seriesResidueProj N hN j :=
116   seriesFourierAverage_eq_residueProj N hN omega omega⁻¹ (N : R)⁻¹
117     (primitiveRoot_finiteRingFourierCertificate N hN omega homega) j
118 
119 end Komorebi.Residue
120 #print axioms Komorebi.Residue.seriesFourierAverage_eq_residueProj
121 #print axioms Komorebi.Residue.primitiveRoot_finiteRingFourierCertificate
122 #print axioms Komorebi.Residue.seriesFourierAverage_eq_residueProj_of_primitiveRoot

Back to source controls