HeisenbergNormalForm.lean

1 import PaperXI.HeisenbergGroup
2 
3 /-! Normal forms and signed commutation in the actual coordinate Heisenberg group. -/
4 set_option autoImplicit false
5 
6 namespace PaperXI.Heisenberg
7 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
8 
9 /-- Every group element is a central element followed by a translation and modulation. -/
10 theorem normal_form (g : Element K X) :
11     g = centralElement (g.central - (2 : K)⁻¹ * g.frequency g.position) *
12       (translationElement g.position * modulationElement g.frequency) := by
13   ext <;> simp
14 
15 /-- The modulation-translation sign agrees with `T_x f(u) = f(u+x)`. -/
16 theorem modulation_translation (h2 : (2 : K) ≠ 0)
17     (ξ : Module.Dual K X) (x : X) :
18     modulationElement ξ * translationElement x =
19       centralElement (-ξ x) * (translationElement x * modulationElement ξ) := by
20   ext <;> simp
21   field_simp
22   ring
23 
24 /-- Translation past modulation contributes the positive scalar character. -/
25 theorem translation_modulation (h2 : (2 : K) ≠ 0)
26     (x : X) (ξ : Module.Dual K X) :
27     translationElement x * modulationElement ξ =
28       centralElement (ξ x) * (modulationElement ξ * translationElement x) := by
29   ext <;> simp
30   field_simp
31   ring
32 
33 end PaperXI.Heisenberg

Back to source controls