FourierCovariance.lean

1 import PaperXI.ProjectorTransport
2 import Mathlib.Data.ZMod.Basic
3 
4 /-! The corrected covariance half of Proposition 3.1 under its printed
5 relation F T(a) F⁻¹ = T(q*a). Idempotence and completeness are not asserted here. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FourierCovariance
9 open scoped BigOperators
10 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11 variable {M : ℕ} [NeZero M]
12 
13 def mulPermutation (q : (ZMod M)ˣ) : ZMod M ≃ ZMod M where
14   toFun a := (q : ZMod M) * a
15   invFun a := ((q⁻¹ : (ZMod M)ˣ) : ZMod M) * a
16   left_inv a := by simp [← mul_assoc]
17   right_inv a := by simp [← mul_assoc]
18 
19 def fourierOperator (T : ZMod M → Module.End K V) (χ : ZMod M → K)
20     (j : ZMod M) : Module.End K V :=
21   (M : K)⁻¹ • ∑ a : ZMod M, χ (-j * a) • T a
22 
23 /-- The inverse exponent is forced by reindexing; no primitive-root assumption
24 is needed for this transport identity itself. -/
25 theorem inverse_exponent_covariance (q : (ZMod M)ˣ) (F : V ≃ₗ[K] V)
26     (T : ZMod M → Module.End K V) (χ : ZMod M → K) (j : ZMod M)
27     (h : ∀ a, F.conj (T a) = T ((q : ZMod M) * a)) :
28     F.conj (fourierOperator T χ j) =
29       fourierOperator T χ (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) := by
30   unfold fourierOperator
31   rw [PaperXI.ProjectorTransport.normalized_sum_conjugation (mulPermutation q) F T _ _ h]
32   congr 1
33   apply Finset.sum_congr rfl
34   intro a _
35   congr 2
36   change -j * (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * a) =
37     -(((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) * a
38   ring
39 
40 end PaperXI.FourierCovariance

Back to source controls