HeisenbergProjector.lean

1 import PaperXI.HeisenbergRepresentation
2 import PaperXI.HeisenbergForm
3 import PaperXI.HeisenbergGeometry
4 import PaperXI.SchrodingerUnitary
5 import PaperXI.FiniteFunctionAverage
6 
7 /-! Actual zero-central isotropic lifts and their orthogonal averaging projectors. -/
8 set_option autoImplicit false
9 set_option maxHeartbeats 600000
10 noncomputable section
11 open scoped BigOperators
12 namespace PaperXI.HeisenbergProjector
13 open HeisenbergForm HeisenbergGeometry
14 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
15 
16 def liftHom (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) :
17     Multiplicative L →* Heisenberg.Element K X where
18   toFun a := ⟨a.toAdd.val.1, a.toAdd.val.2, 0⟩
19   map_one' := by ext <;> rfl
20   map_mul' a b := by
21     have hzero : b.toAdd.val.2 a.toAdd.val.1 - a.toAdd.val.2 b.toAdd.val.1 = 0 :=
22       hL a.toAdd.val a.toAdd.property b.toAdd.val b.toAdd.property
23     ext <;> simp [hzero]
24 
25 @[simp] theorem lift_position (L : Submodule K (X × Module.Dual K X))
26     (hL : IsIsotropic form L) (a : Multiplicative L) :
27     (liftHom L hL a).position = a.toAdd.val.1 := rfl
28 
29 @[simp] theorem lift_frequency (L : Submodule K (X × Module.Dual K X))
30     (hL : IsIsotropic form L) (a : Multiplicative L) :
31     (liftHom L hL a).frequency = a.toAdd.val.2 := rfl
32 
33 @[simp] theorem lift_central (L : Submodule K (X × Module.Dual K X))
34     (hL : IsIsotropic form L) (a : Multiplicative L) :
35     (liftHom L hL a).central = 0 := rfl
36 
37 theorem lift_injective (L : Submodule K (X × Module.Dual K X))
38     (hL : IsIsotropic form L) : Function.Injective (liftHom L hL) := by
39   intro a b h
40   apply Multiplicative.toAdd.injective
41   apply Subtype.ext
42   exact Prod.ext (congrArg Heisenberg.Element.position h)
43     (congrArg Heisenberg.Element.frequency h)
44 
45 def liftedSubgroup (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) :
46     Subgroup (Heisenberg.Element K X) := MonoidHom.range (G := Multiplicative L) (liftHom L hL)
47 
48 theorem mem_liftedSubgroup_iff (L : Submodule K (X × Module.Dual K X))
49     (hL : IsIsotropic form L) (a : Heisenberg.Element K X) :
50     a ∈ liftedSubgroup L hL ↔ (a.position, a.frequency) ∈ L ∧ a.central = 0 := by
51   constructor
52   · rintro ⟨b, rfl⟩
53     exact ⟨b.toAdd.property, rfl⟩
54   · rintro ⟨ha, hz⟩
55     refine ⟨Multiplicative.ofAdd ⟨(a.position, a.frequency), ha⟩, ?_⟩
56     ext <;> simp [liftHom, hz]
57 
58 def liftEquiv (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) :
59     Multiplicative L ≃* liftedSubgroup L hL where
60   toFun a := ⟨liftHom L hL a, ⟨a, rfl⟩⟩
61   invFun a := Classical.choose a.property
62   left_inv a := lift_injective L hL (Classical.choose_spec (show
63     liftHom L hL a ∈ MonoidHom.range (G := Multiplicative L) (liftHom L hL) from ⟨a, rfl⟩))
64   right_inv a := Subtype.ext (Classical.choose_spec a.property)
65   map_mul' a b := Subtype.ext ((liftHom L hL).map_mul a b)
66 
67 instance liftedFintype (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L)
68     [Fintype L] : Fintype (liftedSubgroup L hL) :=
69   Fintype.ofEquiv (Multiplicative L) (liftEquiv L hL).toEquiv
70 
71 @[simp] theorem liftEquiv_coe (L : Submodule K (X × Module.Dual K X))
72     (hL : IsIsotropic form L) (a : Multiplicative L) :
73     ((liftEquiv L hL a).val : Heisenberg.Element K X) = liftHom L hL a := rfl
74 
75 def restriction (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
76     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) :
77     Representation ℂ (Multiplicative L) (X → ℂ) :=
78   (Heisenberg.representation ψ h2).comp (liftHom L hL)
79 
80 @[simp] theorem restriction_apply (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
81     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L)
82     (a : Multiplicative L) :
83     restriction ψ h2 L hL a = Schrodinger.operator ψ a.toAdd.val.1 a.toAdd.val.2 0 := rfl
84 
85 def projector (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
86     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
87     (X → ℂ) →ₗ[ℂ] (X → ℂ) := FiniteAverage.average (G := Multiplicative L) (restriction ψ h2 L hL)
88 
89 theorem projector_apply (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
90     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L]
91     (f : X → ℂ) :
92     projector ψ h2 L hL f = (Fintype.card L : ℂ)⁻¹ •
93       ∑ a : L, Schrodinger.operator ψ a.val.1 a.val.2 0 f := by
94   unfold projector
95   rw [FiniteAverage.average_apply, Fintype.card_multiplicative]
96   simp only [restriction_apply]
97   rw [Function.Bijective.sum_comp Multiplicative.toAdd.bijective
98     (fun a : L => Schrodinger.operator ψ a.val.1 a.val.2 0 f)]
99 
100 /-- The same average indexed by the actual lifted subgroup. -/
101 def subgroupProjector (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
102     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
103     (X → ℂ) →ₗ[ℂ] (X → ℂ) :=
104   FiniteAverage.average ((Heisenberg.representation ψ h2).comp (liftedSubgroup L hL).subtype)
105 
106 theorem projector_eq_subgroupProjector (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
107     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
108     projector ψ h2 L hL = subgroupProjector ψ h2 L hL := by
109   apply LinearMap.ext
110   intro f
111   simp only [projector, subgroupProjector, FiniteAverage.average_apply]
112   change (Fintype.card (Multiplicative L) : ℂ)⁻¹ •
113       ∑ a : Multiplicative L, Heisenberg.representation ψ h2 (liftHom L hL a) f =
114     (Fintype.card (liftedSubgroup L hL) : ℂ)⁻¹ •
115       ∑ a : liftedSubgroup L hL, Heisenberg.representation ψ h2 a.val f
116   rw [← Fintype.card_congr (liftEquiv L hL).toEquiv]
117   congr 1
118   exact Function.Bijective.sum_comp (liftEquiv L hL).bijective
119     (fun a : liftedSubgroup L hL => Heisenberg.representation ψ h2 a.val f)
120 
121 theorem idempotent (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
122     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
123     (projector ψ h2 L hL).comp (projector ψ h2 L hL) = projector ψ h2 L hL :=
124   by simpa only [projector] using
125     FiniteAverage.idempotent (G := Multiplicative L) (restriction ψ h2 L hL)
126 
127 theorem range_eq_invariants (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
128     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
129     LinearMap.range (projector ψ h2 L hL) = Representation.invariants (G := Multiplicative L) (restriction ψ h2 L hL) :=
130   by simpa only [projector] using
131     FiniteAverage.range_eq (G := Multiplicative L) (restriction ψ h2 L hL)
132 
133 section Unitary
134 variable [Fintype K] [Fintype X]
135 
136 theorem pairing_invariant (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
137     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L)
138     (a : Multiplicative L) (f g : X → ℂ) :
139     TranslationAverage.pairing (restriction ψ h2 L hL a f) (restriction ψ h2 L hL a g) =
140       TranslationAverage.pairing f g :=
141   SchrodingerUnitary.pairing_invariant ψ a.toAdd.val.1 a.toAdd.val.2 0 f g
142 
143 theorem self_adjoint (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
144     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L]
145     (f g : X → ℂ) :
146     TranslationAverage.pairing (projector ψ h2 L hL f) g =
147       TranslationAverage.pairing f (projector ψ h2 L hL g) := by
148   have h := FiniteFunctionAverage.self_adjoint (G := Multiplicative L) (X := X)
149     (restriction ψ h2 L hL) (by
150       intro a f g
151       simpa only [restriction_apply, TranslationAverage.pairing] using
152         SchrodingerUnitary.pairing_invariant ψ a.toAdd.val.1 a.toAdd.val.2 0 f g) f g
153   simpa only [projector] using h
154 
155 theorem residual_orthogonal (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
156     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L]
157     (f : X → ℂ) {g : X → ℂ} (hg : g ∈ LinearMap.range (projector ψ h2 L hL)) :
158     TranslationAverage.pairing (f - projector ψ h2 L hL f) g = 0 := by
159   have hfix : projector ψ h2 L hL g = g := by
160     obtain ⟨w, rfl⟩ := hg
161     have h := congrArg (fun T : (X → ℂ) →ₗ[ℂ] (X → ℂ) => T w)
162       (idempotent ψ h2 L hL)
163     exact h
164   have hsub (a b c : X → ℂ) :
165       TranslationAverage.pairing (a-b) c =
166         TranslationAverage.pairing a c - TranslationAverage.pairing b c := by
167     simp [TranslationAverage.pairing, star_sub, sub_mul, Finset.sum_sub_distrib]
168   rw [hsub, self_adjoint ψ h2 L hL, hfix, sub_self]
169 
170 end Unitary
171 
172 /-- The position axis in X plus its dual. -/
173 def positionSpace : Submodule K (X × Module.Dual K X) where
174   carrier := {v | v.2 = 0}
175   zero_mem' := rfl
176   add_mem' hu hv := by simp_all
177   smul_mem' a v hv := by simp_all
178 
179 def positionEquiv : X ≃ₗ[K] positionSpace (K := K) (X := X) where
180   toFun x := ⟨(x, 0), rfl⟩
181   invFun v := v.val.1
182   left_inv _ := rfl
183   right_inv v := by apply Subtype.ext; exact Prod.ext rfl v.property.symm
184   map_add' x y := by apply Subtype.ext; simp
185   map_smul' a x := by apply Subtype.ext; simp
186 
187 instance positionFintype [Fintype X] : Fintype (positionSpace (K := K) (X := X)) :=
188   Fintype.ofEquiv X positionEquiv.toEquiv
189 
190 theorem position_isotropic : IsIsotropic form (positionSpace (K := K) (X := X)) := by
191   intro v hv w hw
192   change v.2 = 0 at hv
193   change w.2 = 0 at hw
194   simp [hv, hw]
195 
196 theorem position_projector_apply [Fintype X] (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0)
197     (f : X → ℂ) (u : X) :
198     projector ψ h2 (positionSpace (K := K) (X := X)) position_isotropic f u = TranslationAverage.mean f := by
199   rw [projector_apply]
200   simp only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul]
201   have hcard := Fintype.card_congr (positionEquiv (K := K) (X := X)).toEquiv
202   rw [← hcard]
203   unfold TranslationAverage.mean
204   congr 1
205   have hsum : (∑ a : positionSpace (K := K) (X := X),
206       Schrodinger.operator ψ a.val.1 a.val.2 0 f u) = ∑ x : X, f (u + x) := by
207     rw [← Function.Bijective.sum_comp (positionEquiv (K := K) (X := X)).bijective
208       (fun a : positionSpace (K := K) (X := X) =>
209         Schrodinger.operator ψ a.val.1 a.val.2 0 f u)]
210     simp [positionEquiv, Schrodinger.operator_apply]
211   rw [hsum]
212   exact Function.Bijective.sum_comp (AddGroup.addLeft_bijective u) f
213 
214 theorem position_projector_eq [Fintype X] (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) :
215     projector ψ h2 (positionSpace (K := K) (X := X)) position_isotropic =
216       FiniteAverage.average (TranslationAverage.translation (X := X)) := by
217   ext f u
218   rw [position_projector_apply, TranslationAverage.average_apply]
219 
220 theorem position_range_eq [Fintype X] (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) :
221     LinearMap.range (projector ψ h2 (positionSpace (K := K) (X := X)) position_isotropic) =
222       TranslationAverage.constantSubmodule := by
223   rw [position_projector_eq, TranslationAverage.range_eq]
224 
225 theorem position_rank_one [Fintype X] (ψ : AddChar K ℂ) (h2 : (2 : K) ≠ 0) :
226     Module.finrank ℂ (LinearMap.range (projector ψ h2 (positionSpace (K := K) (X := X)) position_isotropic)) = 1 := by
227   rw [position_projector_eq]
228   exact TranslationAverage.finrank_range
229 
230 end PaperXI.HeisenbergProjector

Back to source controls