FiniteAnalytic.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV.CyclicFilters
7 import KomorebiPaperIV.SectionCycles
8 import Mathlib.RingTheory.RootsOfUnity.Complex
9 
10 /-!
11 # Finite root-of-unity representations
12 
13 This file connects the coefficient-defined cyclic projector used elsewhere in
14 the Paper IV checkpoint to the explicit finite Fourier average over a primitive
15 root of unity.  Specializing the input series to the formal exponential gives
16 the transfer sections.  Rescaling by an `N`th root of `-1` gives the signed
17 sections and, in residue zero, the distinguished denominator representation.
18 
19 The results here are identities of formal power series.  They do not assert
20 analytic convergence, holomorphy, or pointwise evaluation of those series.
21 -/
22 
23 namespace Komorebi.PaperIV
24 
25 open scoped PowerSeries
26 
27 noncomputable section
28 
29 /-- The finite Fourier average of a formal power series over powers of `omega`. -/
30 def finiteRootAverage (N j : ℕ) (omega : ℂ) (f : ℂ⟦X⟧) : ℂ⟦X⟧ :=
31   PowerSeries.C ((N : ℂ)⁻¹) *
32     ∑ ell ∈ Finset.range N,
33       PowerSeries.C (((omega ^ j)⁻¹) ^ ell) *
34         PowerSeries.rescale (omega ^ ell) f
35 
36 private theorem finite_geometric_sum_filter {N j n : ℕ} (hN : 0 < N)
37     {omega : ℂ} (homega : IsPrimitiveRoot omega N) :
38     ∑ ell ∈ Finset.range N,
39         (((omega ^ j)⁻¹) ^ ell * (omega ^ ell) ^ n) =
40       if n % N = j % N then (N : ℂ) else 0 := by
41   let b : ℂ := (omega ^ j)⁻¹ * omega ^ n
42   have homega0 : omega ≠ 0 := homega.ne_zero hN.ne'
43   have hsummand (ell : ℕ) :
44       ((omega ^ j)⁻¹) ^ ell * (omega ^ ell) ^ n = b ^ ell := by
45     simp only [b, ← pow_mul, mul_pow]
46     rw [Nat.mul_comm ell n]
47   simp_rw [hsummand]
48   have hb_one_iff : b = 1 ↔ n % N = j % N := by
49     rw [show b = (omega ^ j)⁻¹ * omega ^ n by rfl,
50       inv_mul_eq_one₀ (pow_ne_zero j homega0)]
51     rw [eq_comm]
52     simpa only [homega.eq_orderOf, Nat.ModEq] using
53       (homega.isOfFinOrder hN.ne').pow_eq_pow_iff_modEq (n := n) (m := j)
54   have hbpow : b ^ N = 1 := by
55     simp only [b, mul_pow, inv_pow, ← pow_mul]
56     rw [mul_comm j N, mul_comm n N, pow_mul, pow_mul, homega.pow_eq_one]
57     simp
58   by_cases hres : n % N = j % N
59   · have hb : b = 1 := hb_one_iff.2 hres
60     simp [hres, hb]
61   · have hbne : b ≠ 1 := fun hb => hres (hb_one_iff.1 hb)
62     have hmul : (b - 1) * ∑ ell ∈ Finset.range N, b ^ ell = 0 := by
63       rw [mul_geom_sum, hbpow, sub_self]
64     have hsum : ∑ ell ∈ Finset.range N, b ^ ell = 0 :=
65       (mul_eq_zero.mp hmul).resolve_left (sub_ne_zero.mpr hbne)
66     simp [hres, hsum]
67 
68 @[simp]
69 theorem coeff_finiteRootAverage {N : ℕ} (hN : 0 < N) (j n : ℕ)
70     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (f : ℂ⟦X⟧) :
71     PowerSeries.coeff n (finiteRootAverage N j omega f) =
72       if n % N = j % N then PowerSeries.coeff n f else 0 := by
73   rw [finiteRootAverage, PowerSeries.coeff_C_mul, map_sum]
74   simp only [PowerSeries.coeff_C_mul, PowerSeries.coeff_rescale]
75   simp_rw [← mul_assoc]
76   rw [← Finset.sum_mul]
77   rw [finite_geometric_sum_filter hN homega]
78   by_cases hres : n % N = j % N
79   · simp [hres, Nat.cast_ne_zero.mpr hN.ne']
80   · simp [hres]
81 
82 /-- The explicit finite root average agrees with the coefficient projector. -/
83 theorem finiteRootAverage_eq_cyclicProjector {N : ℕ} (hN : 0 < N) (j : ℕ)
84     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (f : ℂ⟦X⟧) :
85     finiteRootAverage N j omega f = cyclicProjector N j f := by
86   ext n
87   rw [coeff_finiteRootAverage hN j n homega, coeff_cyclicProjector]
88 
89 /-- Root-of-unity averaging of the formal exponential gives a transfer section. -/
90 theorem finiteRootAverage_exp_eq_transferSection {N : ℕ} (hN : 0 < N)
91     {j : ℕ} (hjN : j < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N) :
92     finiteRootAverage N j omega (PowerSeries.exp ℂ) =
93       transferSection N j (1 : ℂ) := by
94   ext n
95   rw [coeff_finiteRootAverage hN j n homega, coeff_transferSection]
96   simp only [PowerSeries.coeff_exp, transferSectionCoeff]
97   rw [Nat.mod_eq_of_lt hjN]
98   by_cases hres : n % N = j
99   · simp [hres]
100   · simp [hres]
101 
102 /-- Root-of-unity averaging of a rescaled formal exponential gives the
103 corresponding transfer section. -/
104 theorem finiteRootAverage_rescale_exp_eq_transferSection {N : ℕ} (hN : 0 < N)
105     {j : ℕ} (hjN : j < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N)
106     (rho : ℂ) :
107     finiteRootAverage N j omega
108         (PowerSeries.rescale rho (PowerSeries.exp ℂ)) =
109       transferSection N j rho := by
110   ext n
111   rw [coeff_finiteRootAverage hN j n homega, coeff_transferSection]
112   simp only [PowerSeries.coeff_rescale, PowerSeries.coeff_exp, transferSectionCoeff]
113   rw [Nat.mod_eq_of_lt hjN]
114   by_cases hres : n % N = j
115   · simp [hres]
116   · simp [hres]
117 
118 private theorem signedSectionCoeff_eq_inv_pow_mul_transferSectionCoeff
119     {N j n : ℕ} (hN : 0 < N) (hjN : j < N) {rho : ℂ}
120     (hrho : rho ^ N = -1) :
121     signedSectionCoeff (R := ℂ) N j n =
122       (rho ^ j)⁻¹ * transferSectionCoeff N j rho n := by
123   have hrho0 : rho ≠ 0 := by
124     intro hzero
125     subst rho
126     simp [hN.ne'] at hrho
127   rw [signedSectionCoeff, transferSectionCoeff]
128   by_cases hres : n % N = j
129   · simp only [hres, ↓reduceIte]
130     have hn : n = N * (n / N) + j := by
131       calc
132         n = N * (n / N) + n % N := (Nat.div_add_mod n N).symm
133         _ = N * (n / N) + j := by rw [hres]
134     have hdiv : (N * (n / N) + j) / N = n / N := by
135       rw [Nat.add_comm, Nat.add_mul_div_left j (n / N) hN,
136         Nat.div_eq_of_lt hjN, zero_add]
137     rw [hn, hdiv, pow_add, pow_mul, hrho]
138     field_simp
139   · simp [hres]
140 
141 /-- A chosen `N`th root of `-1` converts transfer sections into signed
142 sections, including the normalizing factor `rho ^ (-j)`. -/
143 theorem signedSection_eq_inv_pow_mul_transferSection {N : ℕ} (hN : 0 < N)
144     {j : ℕ} (hjN : j < N) {rho : ℂ} (hrho : rho ^ N = -1) :
145     signedSection (R := ℂ) N j =
146       PowerSeries.C ((rho ^ j)⁻¹) * transferSection N j rho := by
147   ext n
148   rw [PowerSeries.coeff_C_mul, coeff_signedSection, coeff_transferSection,
149     signedSectionCoeff_eq_inv_pow_mul_transferSectionCoeff hN hjN hrho]
150   rw [mul_assoc]
151 
152 /-- The general formal finite exponential representation of a signed section. -/
153 theorem signedSection_eq_finiteRootAverage_rescale_exp {N : ℕ} (hN : 0 < N)
154     {j : ℕ} (hjN : j < N) {omega rho : ℂ}
155     (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) :
156     signedSection (R := ℂ) N j =
157       PowerSeries.C ((rho ^ j)⁻¹) *
158         finiteRootAverage N j omega
159           (PowerSeries.rescale rho (PowerSeries.exp ℂ)) := by
160   rw [signedSection_eq_inv_pow_mul_transferSection hN hjN hrho,
161     finiteRootAverage_rescale_exp_eq_transferSection hN hjN homega]
162 
163 /-- Residue zero expands as the unweighted average over the `N` roots
164 `rho * omega ^ ell` of `-1`, the formal counterpart of the distinguished
165 denominator's finite exponential representation. -/
166 theorem signedSection_zero_eq_finite_exponential_average {N : ℕ} (hN : 0 < N)
167     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) :
168     signedSection (R := ℂ) N 0 =
169       PowerSeries.C ((N : ℂ)⁻¹) *
170         ∑ ell ∈ Finset.range N,
171           PowerSeries.rescale (rho * omega ^ ell) (PowerSeries.exp ℂ) := by
172   rw [signedSection_eq_finiteRootAverage_rescale_exp hN (Nat.zero_lt_of_lt hN)
173     homega hrho]
174   simp [finiteRootAverage, PowerSeries.rescale_rescale]
175 
176 end
177 
178 end Komorebi.PaperIV

Back to source controls