FourierPackets.lean

1 import PaperXI.FourierProjectors
2 
3 /-! The ranges of the computed projectors are precisely the declared character
4 spaces. This identifies the algebraic operators with the paper's tame packets. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.FourierPackets
8 open scoped BigOperators
9 open PaperXI.CyclicAction PaperXI.FourierProjectors
10 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11 variable {M : ℕ} [NeZero M]
12 
13 def packet (ρ : Action (K := K) (V := V) (M := M))
14     (ψ : AddChar (ZMod M) K) (j : ZMod M) : Submodule K V where
15   carrier := {v | ∀ a, operator ρ a v = ψ (j * a) • v}
16   zero_mem' := by simp
17   add_mem' hx hy := by intro a; simp [hx a, hy a, smul_add]
18   smul_mem' c x hx := by intro a; simp [hx a, smul_smul, mul_comm]
19 
20 theorem projector_mem_packet (ρ : Action (K := K) (V := V) (M := M))
21     (ψ : AddChar (ZMod M) K) (j : ZMod M) (v : V) :
22     projector ρ ψ j v ∈ packet ρ ψ j := by
23   intro a
24   have h := LinearMap.congr_fun (action_projector ρ ψ j a) v
25   simpa [Module.End.mul_apply] using h
26 
27 theorem projector_on_packet (ρ : Action (K := K) (V := V) (M := M))
28     (ψ : AddChar (ZMod M) K) (hM : (M : K) ≠ 0)
29     (j : ZMod M) {v : V} (hv : v ∈ packet ρ ψ j) : projector ρ ψ j v = v := by
30   change ∀ a, operator ρ a v = ψ (j * a) • v at hv
31   rw [projector_formula, LinearMap.smul_apply, LinearMap.sum_apply]
32   simp_rw [LinearMap.smul_apply, hv, smul_smul, ← AddChar.map_add_eq_mul]
33   rw [← Finset.sum_smul]
34   simp [neg_mul, smul_smul, hM]
35 
36 theorem projector_range (ρ : Action (K := K) (V := V) (M := M))
37     (ψ : AddChar (ZMod M) K) (hM : (M : K) ≠ 0) (j : ZMod M) :
38     LinearMap.range (projector ρ ψ j) = packet ρ ψ j := by
39   ext v
40   constructor
41   · rintro ⟨w, rfl⟩; exact projector_mem_packet ρ ψ j w
42   · intro hv; exact ⟨v, projector_on_packet ρ ψ hM j hv⟩
43 
44 theorem vector_reconstruction (ρ : Action (K := K) (V := V) (M := M))
45     (ψ : AddChar (ZMod M) K) (hψ : ψ.IsPrimitive) (hM : (M : K) ≠ 0) (v : V) :
46     (∑ j : ZMod M, projector ρ ψ j v) = v := by
47   have h := LinearMap.congr_fun (projector_complete ρ ψ hψ hM) v
48   simpa using h
49 
50 end PaperXI.FourierPackets

Back to source controls