IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Tendsto4D
IndisputableMonolith/Gravity/Analysis/ReggeBlochM2Tendsto4D.lean · 270 lines · 19 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
3import IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit
4
5/-!
6# Close `FoldAlongM2Tendsto` for axis TT and pure gauge
7
8Uses the proved cosine two-jet
9`ReggeTTContinuumLimit.cos_sub_one_div_sq_tendsto` and the already-proved
10zero-momentum vanishing of the deficit kernel on `axisTTPlus` /
11`decoyGauge`.
12
13Honest scope: closes the punctured Tendsto along `symbolDir` for those
14two polarizations. General `H` remains the named Prop from the symbol
15module.
16-/
17
18namespace IndisputableMonolith
19namespace Gravity
20namespace Analysis
21namespace ReggeBlochM2Tendsto4D
22
23open BigOperators Filter Topology
24open ReggeEdgeStencil4D
25open ReggeBlochFold4D
26open ReggeBlochM2Symbol4D
27open ReggeFlat4DHessianAssembly
28open ReggeTTContinuumLimit
29open EdgeTTDecomposition4D
30
31noncomputable section
32
33def areaAlong (H : Mat4) (s : Fin 24) (t : Fin 10) (μ : ℝ) : ℝ :=
34 phasedClassDot (slotAreaCov s t) H (fun i => μ * symbolDir i) (hingeBase s t)
35
36def kerAlong (H : Mat4) (s : Fin 24) (t : Fin 10) (μ : ℝ) : ℝ :=
37 phasedClassDot (slotDeficitKer s t) H (fun i => μ * symbolDir i) (hingeBase s t)
38
39theorem areaAlong_eq (H : Mat4) (s : Fin 24) (t : Fin 10) (μ : ℝ) :
40 areaAlong H s t μ =
41 ∑ d : Fin 15,
42 slotAreaCov s t d * classCoeff H d *
43 Real.cos (μ * phaseScale (hingeBase s t) d) := by
44 simpa [areaAlong] using phasedClassDot_symbolDir (slotAreaCov s t) H μ (hingeBase s t)
45
46theorem kerAlong_eq (H : Mat4) (s : Fin 24) (t : Fin 10) (μ : ℝ) :
47 kerAlong H s t μ =
48 ∑ d : Fin 15,
49 slotDeficitKer s t d * classCoeff H d *
50 Real.cos (μ * phaseScale (hingeBase s t) d) := by
51 simpa [kerAlong] using
52 phasedClassDot_symbolDir (slotDeficitKer s t) H μ (hingeBase s t)
53
54theorem areaAlong_zero (H : Mat4) (s : Fin 24) (t : Fin 10) :
55 areaAlong H s t 0 =
56 ∑ d : Fin 15, slotAreaCov s t d * classCoeff H d := by
57 simp [areaAlong_eq, Real.cos_zero]
58
59theorem kerAlong_zero (H : Mat4) (s : Fin 24) (t : Fin 10) :
60 kerAlong H s t 0 =
61 ∑ d : Fin 15, slotDeficitKer s t d * classCoeff H d := by
62 simp [kerAlong_eq, Real.cos_zero]
63
64theorem kerAlong_axis_zero (s : Fin 24) (t : Fin 10) :
65 kerAlong axisTTPlus s t 0 = 0 := by
66 rw [kerAlong_zero]
67 simpa [classDot] using classDot_slotDeficitKer_axis s t
68
69theorem kerAlong_gauge_zero (s : Fin 24) (t : Fin 10) :
70 kerAlong decoyGauge s t 0 = 0 := by
71 rw [kerAlong_zero]
72 simpa [classDot] using classDot_slotDeficitKer_gauge s t
73
74/-- Formal second-jet coefficient of `kerAlong` after using `K(0)=0`. -/
75def kerM2Coeff (H : Mat4) (s : Fin 24) (t : Fin 10) : ℝ :=
76 -(1 / 2 : ℝ) *
77 ∑ d : Fin 15,
78 slotDeficitKer s t d * classCoeff H d *
79 (phaseScale (hingeBase s t) d) ^ 2
80
81theorem tendsto_kerAlong_div_sq (H : Mat4) (s : Fin 24) (t : Fin 10)
82 (h0 : kerAlong H s t 0 = 0) :
83 Tendsto (fun μ : ℝ => kerAlong H s t μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
84 (𝓝 (kerM2Coeff H s t)) := by
85 have hcongr :
86 (fun μ : ℝ => kerAlong H s t μ / μ ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
87 fun μ : ℝ =>
88 ∑ d : Fin 15,
89 (slotDeficitKer s t d * classCoeff H d) *
90 ((Real.cos (μ * phaseScale (hingeBase s t) d) - 1) / μ ^ 2) := by
91 filter_upwards [self_mem_nhdsWithin] with μ hμ
92 have hne : μ ≠ 0 := hμ
93 have hK := kerAlong_eq H s t μ
94 have hsum0 : kerAlong H s t 0 = 0 := h0
95 rw [kerAlong_zero] at hsum0
96 have hrewrite :
97 kerAlong H s t μ / μ ^ 2 =
98 (∑ d : Fin 15,
99 slotDeficitKer s t d * classCoeff H d *
100 (Real.cos (μ * phaseScale (hingeBase s t) d) - 1)) / μ ^ 2 := by
101 rw [hK]
102 have hsub :
103 (∑ d : Fin 15,
104 slotDeficitKer s t d * classCoeff H d *
105 Real.cos (μ * phaseScale (hingeBase s t) d)) -
106 (∑ d : Fin 15, slotDeficitKer s t d * classCoeff H d) =
107 ∑ d : Fin 15,
108 slotDeficitKer s t d * classCoeff H d *
109 (Real.cos (μ * phaseScale (hingeBase s t) d) - 1) := by
110 simp [Finset.sum_sub_distrib, mul_sub]
111 calc
112 (∑ d : Fin 15,
113 slotDeficitKer s t d * classCoeff H d *
114 Real.cos (μ * phaseScale (hingeBase s t) d)) / μ ^ 2
115 =
116 ((∑ d : Fin 15,
117 slotDeficitKer s t d * classCoeff H d *
118 Real.cos (μ * phaseScale (hingeBase s t) d)) -
119 (∑ d : Fin 15, slotDeficitKer s t d * classCoeff H d)) /
120 μ ^ 2 := by rw [hsum0, sub_zero]
121 _ = (∑ d : Fin 15,
122 slotDeficitKer s t d * classCoeff H d *
123 (Real.cos (μ * phaseScale (hingeBase s t) d) - 1)) /
124 μ ^ 2 := by rw [hsub]
125 rw [hrewrite, Finset.sum_div]
126 refine Finset.sum_congr rfl fun d _ => ?_
127 field_simp [hne]
128 have hsum :
129 Tendsto
130 (fun μ : ℝ =>
131 ∑ d : Fin 15,
132 (slotDeficitKer s t d * classCoeff H d) *
133 ((Real.cos (μ * phaseScale (hingeBase s t) d) - 1) / μ ^ 2))
134 (𝓝[≠] (0 : ℝ))
135 (𝓝
136 (∑ d : Fin 15,
137 (slotDeficitKer s t d * classCoeff H d) *
138 (-(phaseScale (hingeBase s t) d) ^ 2 / 2))) := by
139 apply tendsto_finset_sum
140 intro d _
141 exact
142 (cos_sub_one_div_sq_tendsto (phaseScale (hingeBase s t) d)).const_mul _
143 have htarget :
144 (∑ d : Fin 15,
145 (slotDeficitKer s t d * classCoeff H d) *
146 (-(phaseScale (hingeBase s t) d) ^ 2 / 2)) =
147 kerM2Coeff H s t := by
148 unfold kerM2Coeff
149 simp [div_eq_mul_inv, Finset.mul_sum, mul_left_comm, mul_assoc, mul_comm]
150 rw [← htarget]
151 exact (tendsto_congr' hcongr).mpr hsum
152
153theorem continuous_areaAlong (H : Mat4) (s : Fin 24) (t : Fin 10) :
154 Continuous (areaAlong H s t) := by
155 have hfun :
156 areaAlong H s t =
157 fun μ : ℝ =>
158 ∑ d : Fin 15,
159 slotAreaCov s t d * classCoeff H d *
160 Real.cos (μ * phaseScale (hingeBase s t) d) := by
161 funext μ; exact areaAlong_eq H s t μ
162 rw [hfun]
163 refine continuous_finset_sum _ fun d _ => ?_
164 continuity
165
166theorem tendsto_slot_product (H : Mat4) (s : Fin 24) (t : Fin 10)
167 (h0 : kerAlong H s t 0 = 0) :
168 Tendsto
169 (fun μ : ℝ => areaAlong H s t μ * kerAlong H s t μ / μ ^ 2)
170 (𝓝[≠] (0 : ℝ))
171 (𝓝 (areaAlong H s t 0 * kerM2Coeff H s t)) := by
172 have hK := tendsto_kerAlong_div_sq H s t h0
173 have hA :
174 Tendsto (areaAlong H s t) (𝓝[≠] (0 : ℝ)) (𝓝 (areaAlong H s t 0)) :=
175 ((continuous_areaAlong H s t).tendsto 0).mono_left nhdsWithin_le_nhds
176 have hprod := Tendsto.mul hA hK
177 have hcongr :
178 (fun μ : ℝ => areaAlong H s t μ * (kerAlong H s t μ / μ ^ 2)) =ᶠ[
179 𝓝[≠] (0 : ℝ)]
180 fun μ : ℝ => areaAlong H s t μ * kerAlong H s t μ / μ ^ 2 := by
181 filter_upwards with μ
182 ring
183 exact (tendsto_congr' hcongr).mp hprod
184
185theorem m2SlotCoeff_eq_area_kerM2 (H : Mat4) (s : Fin 24) (t : Fin 10) :
186 m2SlotCoeff H s t =
187 (if isT11 s t then areaAlong H s t 0 * kerM2Coeff H s t else 0) := by
188 unfold m2SlotCoeff kerM2Coeff
189 by_cases ht : isT11 s t
190 · simp [ht, areaAlong_zero]
191 · simp [ht]
192
193theorem tendsto_transportedSlotTerm_div_sq (H : Mat4) (s : Fin 24) (t : Fin 10)
194 (h0 : kerAlong H s t 0 = 0) :
195 Tendsto
196 (fun μ : ℝ =>
197 transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2)
198 (𝓝[≠] (0 : ℝ)) (𝓝 (m2SlotCoeff H s t)) := by
199 by_cases ht : isT11 s t
200 · have hterm :
201 (fun μ : ℝ =>
202 transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2) =
203 fun μ : ℝ => areaAlong H s t μ * kerAlong H s t μ / μ ^ 2 := by
204 funext μ
205 simp [transportedSlotTerm, ht, areaAlong, kerAlong]
206 rw [hterm, m2SlotCoeff_eq_area_kerM2 H s t, if_pos ht]
207 exact tendsto_slot_product H s t h0
208 · have hterm :
209 (fun μ : ℝ =>
210 transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2) =
211 fun _ : ℝ => (0 : ℝ) := by
212 funext μ
213 simp [transportedSlotTerm, ht]
214 rw [hterm, m2SlotCoeff_eq_area_kerM2 H s t, if_neg ht]
215 exact tendsto_const_nhds
216
217theorem tendsto_foldAlong_div_sq (H : Mat4)
218 (h0 : ∀ s t, kerAlong H s t 0 = 0) :
219 Tendsto (fun μ : ℝ => foldAlong H μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
220 (𝓝 (m2Symbol H)) := by
221 have hsum :
222 Tendsto
223 (fun μ : ℝ =>
224 ∑ s : Fin 24, ∑ t : Fin 10,
225 transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2)
226 (𝓝[≠] (0 : ℝ))
227 (𝓝 (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCoeff H s t)) := by
228 apply tendsto_finset_sum
229 intro s _
230 apply tendsto_finset_sum
231 intro t _
232 exact tendsto_transportedSlotTerm_div_sq H s t (h0 s t)
233 have hcongr :
234 (fun μ : ℝ => foldAlong H μ / μ ^ 2) =ᶠ[𝓝[≠] (0 : ℝ)]
235 fun μ : ℝ =>
236 ∑ s : Fin 24, ∑ t : Fin 10,
237 transportedSlotTerm H (fun i => μ * symbolDir i) s t / μ ^ 2 := by
238 filter_upwards [self_mem_nhdsWithin] with μ hμ
239 have hne : μ ≠ 0 := hμ
240 unfold foldAlong blochFold11
241 rw [Finset.sum_div]
242 refine Finset.sum_congr rfl fun s _ => ?_
243 rw [Finset.sum_div]
244 exact (tendsto_congr' hcongr).mpr (by simpa [m2Symbol] using hsum)
245
246theorem FoldAlongM2Tendsto_of_axisTTPlus :
247 FoldAlongM2Tendsto axisTTPlus := by
248 unfold FoldAlongM2Tendsto
249 exact tendsto_foldAlong_div_sq axisTTPlus fun s t => kerAlong_axis_zero s t
250
251theorem FoldAlongM2Tendsto_of_decoyGauge :
252 FoldAlongM2Tendsto decoyGauge := by
253 unfold FoldAlongM2Tendsto
254 exact tendsto_foldAlong_div_sq decoyGauge fun s t => kerAlong_gauge_zero s t
255
256theorem FoldAlongM2Tendsto_axisTTPlus_holds :
257 FoldAlongM2Tendsto_axisTTPlus :=
258 (FoldAlongM2Tendsto_axis_iff).mp FoldAlongM2Tendsto_of_axisTTPlus
259
260theorem FoldAlongM2Tendsto_decoyGauge_holds :
261 FoldAlongM2Tendsto_decoyGauge :=
262 (FoldAlongM2Tendsto_gauge_iff).mp FoldAlongM2Tendsto_of_decoyGauge
263
264end
265
266end ReggeBlochM2Tendsto4D
267end Analysis
268end Gravity
269end IndisputableMonolith
270