IndisputableMonolith.Geometry.ReggeActionNonlinearHessianProof
IndisputableMonolith/Geometry/ReggeActionNonlinearHessianProof.lean · 2372 lines · 142 declarations
show as:
view math explainer →
1import IndisputableMonolith.Geometry.ReggeActionSecondVariation
2
3/-!
4# Nonlinear Regge Hessian Proof Interface
5
6This module isolates the remaining hard calculation for the full nonlinear
7Regge action: the second directional derivative at the flat potential must
8equal the canonical incidence Hessian.
9
10The theorem below is not a new assumption; it is the exact endpoint of the
11second chain-rule calculation. Once that calculation is supplied, the existing
12`ReggeActionSecondVariationInput` follows immediately.
13-/
14
15namespace IndisputableMonolith
16namespace Geometry
17namespace ReggeActionNonlinearHessianProof
18
19open ReggeTriangulation3D
20open ReggeHessian3D
21open Triangulation3DConsistency
22open ReggeActionConcrete
23open ReggeActionSmoothness
24open ReggeActionSecondVariation
25
26noncomputable section
27
28theorem differentiableAt_eventually_of_contDiffAt_top
29 (f : ℝ → ℝ) (x : ℝ)
30 (h : ContDiffAt ℝ (⊤ : ℕ∞) f x) :
31 ∀ᶠ y : ℝ in nhds x, DifferentiableAt ℝ f y := by
32 rcases h.contDiffOn (m := (1 : ℕ∞)) (by simp)
33 (by intro htop; simp at htop) with ⟨u, hu, hcu⟩
34 rcases mem_nhds_iff.mp hu with ⟨v, hvu, hvopen, hxv⟩
35 filter_upwards [IsOpen.eventually_mem hvopen hxv] with y hy
36 have huy : u ∈ nhds y :=
37 Filter.mem_of_superset (IsOpen.mem_nhds hvopen hy) hvu
38 exact (hcu.differentiableOn (by simp)).differentiableAt huy
39
40theorem deriv_differentiableAt_of_contDiffAt_top
41 (f : ℝ → ℝ) (x : ℝ)
42 (h : ContDiffAt ℝ (⊤ : ℕ∞) f x) :
43 DifferentiableAt ℝ (fun y : ℝ => deriv f y) x := by
44 have htop : (1 : WithTop ℕ∞) + 1 ≤ ((⊤ : ℕ∞) : WithTop ℕ∞) := by
45 exact WithTop.coe_le_coe.2 (by exact le_top)
46 have hfderiv : ContDiffAt ℝ (1 : ℕ∞) (fderiv ℝ f) x := by
47 exact h.fderiv_right htop
48 have hdiffF : DifferentiableAt ℝ (fderiv ℝ f) x := by
49 exact hfderiv.differentiableAt (by norm_num)
50 change DifferentiableAt ℝ (fun y : ℝ => (fderiv ℝ f y) 1) x
51 exact ((ContinuousLinearMap.apply ℝ ℝ (1 : ℝ)).differentiableAt.comp x hdiffF)
52
53theorem hasSecondDerivAt_const_add
54 (f : ℝ → ℝ) (c d2 x : ℝ)
55 (h : HasSecondDerivAt f d2 x) :
56 HasSecondDerivAt (fun t : ℝ => c + f t) d2 x := by
57 unfold HasSecondDerivAt at h ⊢
58 have hderiv :
59 (fun t : ℝ => deriv (fun y : ℝ => c + f y) t) =
60 fun t : ℝ => deriv f t := by
61 funext t
62 exact deriv_const_add (f := f) (x := t) (c := c)
63 simpa [hderiv] using h
64
65/-- Exact second-directional-variation statement for the full nonlinear Regge
66action. -/
67def NonlinearReggeDirectionalHessianTheorem
68 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
69 ∀ ξ : VertexPotential K,
70 HasSecondDerivAt (actionAlongLine K hK ξ)
71 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0
72
73/-- The exact first-derivative linearization that remains after the local
74geometric product rule, Cayley-Menger/arccos derivative, hinge derivative, and
75Schlaefli cancellation are expanded near the flat point. It is stronger than a
76single derivative-at-zero statement and is precisely enough to give the
77nonlinear Hessian. -/
78def ActionDerivativeLinearizationNearZeroTarget
79 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
80 ∀ ξ : VertexPotential K,
81 (fun t : ℝ => deriv (actionAlongLine K hK ξ) t) =ᶠ[nhds (0 : ℝ)]
82 fun t : ℝ => t * hessianQuadratic (canonicalReggeHessian K hK) ξ
83
84/-- The sharp Hessian target: the derivative of the full action along each
85conformal line is tangent at first order to the canonical Hessian line. Unlike
86`ActionDerivativeLinearizationNearZeroTarget`, this allows cubic and higher
87Regge terms. -/
88def ActionDerivativeFirstOrderTangencyTarget
89 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
90 ∀ ξ : VertexPotential K,
91 HasDerivAt
92 (fun t : ℝ =>
93 deriv (actionAlongLine K hK ξ) t -
94 t * hessianQuadratic (canonicalReggeHessian K hK) ξ)
95 0 0
96
97theorem nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency
98 (K : Triangulation3D) (hK : IncidenceConsistent K)
99 (hTan : ActionDerivativeFirstOrderTangencyTarget K hK) :
100 NonlinearReggeDirectionalHessianTheorem K hK := by
101 intro ξ
102 unfold HasSecondDerivAt
103 have hLinear : HasDerivAt
104 (fun t : ℝ => t * hessianQuadratic (canonicalReggeHessian K hK) ξ)
105 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := by
106 simpa using
107 (hasDerivAt_id (0 : ℝ)).mul_const
108 (hessianQuadratic (canonicalReggeHessian K hK) ξ)
109 have hsum := (hTan ξ).add hLinear
110 convert hsum using 1
111 · ext t
112 let q := hessianQuadratic (canonicalReggeHessian K hK) ξ
113 change deriv (actionAlongLine K hK ξ) t =
114 deriv (actionAlongLine K hK ξ) t - t * q + t * q
115 ring
116 · ring
117
118theorem nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero
119 (K : Triangulation3D) (hK : IncidenceConsistent K)
120 (hLin : ActionDerivativeLinearizationNearZeroTarget K hK) :
121 NonlinearReggeDirectionalHessianTheorem K hK := by
122 intro ξ
123 unfold HasSecondDerivAt
124 have hLinear : HasDerivAt
125 (fun t : ℝ => t * hessianQuadratic (canonicalReggeHessian K hK) ξ)
126 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := by
127 simpa using
128 (hasDerivAt_id (0 : ℝ)).mul_const
129 (hessianQuadratic (canonicalReggeHessian K hK) ξ)
130 exact hLinear.congr_of_eventuallyEq (hLin ξ)
131
132theorem actionDerivativeFirstOrderTangency_of_linearizationNearZero
133 (K : Triangulation3D) (hK : IncidenceConsistent K)
134 (hLin : ActionDerivativeLinearizationNearZeroTarget K hK) :
135 ActionDerivativeFirstOrderTangencyTarget K hK := by
136 intro ξ
137 have hzero : HasDerivAt (fun _t : ℝ => (0 : ℝ)) 0 0 :=
138 hasDerivAt_const 0 0
139 refine hzero.congr_of_eventuallyEq ?_
140 filter_upwards [hLin ξ] with t ht
141 rw [ht]
142 ring
143
144/-- The canonical quadratic term restricted to a conformal line. -/
145def canonicalQuadraticAlongLine
146 (K : Triangulation3D) (hK : IncidenceConsistent K)
147 (ξ : VertexPotential K) (t : ℝ) : ℝ :=
148 (1 / 2) *
149 hessianQuadratic (canonicalReggeHessian K hK) (linePotential K ξ t)
150
151/-- The canonical nonlinear remainder restricted to a conformal line. -/
152def canonicalRemainderAlongLine
153 (K : Triangulation3D) (hK : IncidenceConsistent K)
154 (ξ : VertexPotential K) (t : ℝ) : ℝ :=
155 reggeActionRemainder K hK (canonicalReggeHessian K hK)
156 (linePotential K ξ t)
157
158/-- Exact one-dimensional split of the nonlinear Regge action along every
159conformal line. This is the algebraic reduction used by the nonlinear
160Hessian proof: after this point the only remaining analytic content is the
161second variation of the canonical remainder. -/
162theorem actionAlongLine_canonical_split
163 (K : Triangulation3D) (hK : IncidenceConsistent K)
164 (ξ : VertexPotential K) :
165 actionAlongLine K hK ξ =
166 fun t : ℝ =>
167 reggeAction K hK (zeroPotential K) +
168 canonicalQuadraticAlongLine K hK ξ t +
169 canonicalRemainderAlongLine K hK ξ t := by
170 funext t
171 unfold actionAlongLine canonicalQuadraticAlongLine canonicalRemainderAlongLine
172 simpa using
173 reggeAction_taylor_decomposition K hK (canonicalReggeHessian K hK)
174 (linePotential K ξ t)
175
176/-- Equivalent explicit subtraction form of the canonical remainder along a
177line. This is the exact expression whose second derivative must vanish after
178the Cayley-Menger/arccos/hinge chain rule is expanded. -/
179theorem canonicalRemainderAlongLine_eq_action_sub_quadratic
180 (K : Triangulation3D) (hK : IncidenceConsistent K)
181 (ξ : VertexPotential K) :
182 canonicalRemainderAlongLine K hK ξ =
183 fun t : ℝ =>
184 actionAlongLine K hK ξ t -
185 reggeAction K hK (zeroPotential K) -
186 canonicalQuadraticAlongLine K hK ξ t := by
187 funext t
188 unfold canonicalRemainderAlongLine actionAlongLine canonicalQuadraticAlongLine
189 reggeActionRemainder
190 ring
191
192/-- The canonical quadratic line has exactly the canonical Regge Hessian as
193its second directional derivative. -/
194theorem canonicalQuadraticAlongLine_hasSecondDerivAt_zero
195 (K : Triangulation3D) (hK : IncidenceConsistent K)
196 (ξ : VertexPotential K) :
197 HasSecondDerivAt (canonicalQuadraticAlongLine K hK ξ)
198 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := by
199 change HasSecondDerivAt
200 (fun t : ℝ =>
201 (1 / 2) * hessianQuadratic (canonicalReggeHessian K hK)
202 (linePotential K ξ t))
203 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0
204 simpa using
205 hessianQuadratic_along_line_hasSecondDerivAt_zero K
206 (canonicalReggeHessian K hK) ξ
207
208theorem canonicalQuadraticAlongLine_differentiableAt
209 (K : Triangulation3D) (hK : IncidenceConsistent K)
210 (ξ : VertexPotential K) (t : ℝ) :
211 DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t := by
212 have hquad :
213 canonicalQuadraticAlongLine K hK ξ =
214 fun t : ℝ =>
215 (hessianQuadratic (canonicalReggeHessian K hK) ξ / 2) * t ^ 2 := by
216 funext t
217 unfold canonicalQuadraticAlongLine
218 rw [hessianQuadratic_linePotential]
219 ring
220 rw [hquad]
221 exact (((differentiableAt_id : DifferentiableAt ℝ (fun t : ℝ => t) t).pow 2).const_mul
222 (hessianQuadratic (canonicalReggeHessian K hK) ξ / 2))
223
224theorem canonicalQuadraticAlongLine_hasDerivAt
225 (K : Triangulation3D) (hK : IncidenceConsistent K)
226 (ξ : VertexPotential K) (t : ℝ) :
227 HasDerivAt (canonicalQuadraticAlongLine K hK ξ)
228 (t * hessianQuadratic (canonicalReggeHessian K hK) ξ) t := by
229 have hquad :
230 canonicalQuadraticAlongLine K hK ξ =
231 fun t : ℝ =>
232 (hessianQuadratic (canonicalReggeHessian K hK) ξ / 2) * t ^ 2 := by
233 funext t
234 unfold canonicalQuadraticAlongLine
235 rw [hessianQuadratic_linePotential]
236 ring
237 rw [hquad]
238 have hpow := ((hasDerivAt_id t).pow 2).const_mul
239 (hessianQuadratic (canonicalReggeHessian K hK) ξ / 2)
240 simpa [two_mul, mul_comm, mul_left_comm, mul_assoc] using hpow
241
242theorem deriv_canonicalQuadraticAlongLine
243 (K : Triangulation3D) (hK : IncidenceConsistent K)
244 (ξ : VertexPotential K) (t : ℝ) :
245 deriv (canonicalQuadraticAlongLine K hK ξ) t =
246 t * hessianQuadratic (canonicalReggeHessian K hK) ξ :=
247 (canonicalQuadraticAlongLine_hasDerivAt K hK ξ t).deriv
248
249/-- Equivalent geometric target phrased against the actual derivative of the
250canonical quadratic line rather than the simplified scalar formula. -/
251def ActionDerivativeTangencyToQuadraticTarget
252 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
253 ∀ ξ : VertexPotential K,
254 HasDerivAt
255 (fun t : ℝ =>
256 deriv (actionAlongLine K hK ξ) t -
257 deriv (canonicalQuadraticAlongLine K hK ξ) t)
258 0 0
259
260theorem actionDerivativeFirstOrderTangency_of_quadraticTangency
261 (K : Triangulation3D) (hK : IncidenceConsistent K)
262 (hTan : ActionDerivativeTangencyToQuadraticTarget K hK) :
263 ActionDerivativeFirstOrderTangencyTarget K hK := by
264 intro ξ
265 have h := hTan ξ
266 convert h using 1
267 ext t
268 rw [deriv_canonicalQuadraticAlongLine K hK ξ t]
269
270/-- Derivative of the conformal hinge length along a fixed conformal line,
271defined by the one-variable derivative. The remaining geometric product-rule
272work should compute this explicitly near the flat point. -/
273def hingeLineDeriv
274 (K : Triangulation3D) (hK : IncidenceConsistent K)
275 (ξ : VertexPotential K) (e : Fin K.nE) (t : ℝ) : ℝ :=
276 deriv (fun s : ℝ =>
277 hingeMeasureUnderConformal K hK (linePotential K ξ s) e) t
278
279/-- Derivative of the deficit angle along a fixed conformal line, defined by
280the one-variable derivative. The remaining local cofactor/arccos derivative
281work should compute this explicitly near the flat point. -/
282def deficitLineDeriv
283 (K : Triangulation3D)
284 (ξ : VertexPotential K) (e : Fin K.nE) (t : ℝ) : ℝ :=
285 deriv (fun s : ℝ => deficitAngle K (linePotential K ξ s) e) t
286
287/-- Second derivative of the conformal hinge length along a fixed conformal
288line, expressed as the derivative of `hingeLineDeriv`. -/
289def hingeLineSecondDeriv
290 (K : Triangulation3D) (hK : IncidenceConsistent K)
291 (ξ : VertexPotential K) (e : Fin K.nE) (t : ℝ) : ℝ :=
292 deriv (fun s : ℝ => hingeLineDeriv K hK ξ e s) t
293
294/-- Second derivative of the deficit angle along a fixed conformal line,
295expressed as the derivative of `deficitLineDeriv`. -/
296def deficitLineSecondDeriv
297 (K : Triangulation3D)
298 (ξ : VertexPotential K) (e : Fin K.nE) (t : ℝ) : ℝ :=
299 deriv (fun s : ℝ => deficitLineDeriv K ξ e s) t
300
301/-- Product-rule expression for the derivative of the full Regge action along
302a conformal line. This is the exact finite-sum expression obtained after
303differentiating the hinge factor and the deficit factor. -/
304def reggeActionProductRuleDerivative
305 (K : Triangulation3D) (hK : IncidenceConsistent K)
306 (ξ : VertexPotential K) (t : ℝ) : ℝ :=
307 ∑ e : Fin K.nE,
308 (hingeLineDeriv K hK ξ e t *
309 deficitAngle K (linePotential K ξ t) e +
310 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
311 deficitLineDeriv K ξ e t)
312
313/-- Derivative of the product-rule expression, before using Schlaefli and the
314Cayley-Menger/arccos algebra. -/
315def reggeActionSecondProductRuleDerivative
316 (K : Triangulation3D) (hK : IncidenceConsistent K)
317 (ξ : VertexPotential K) (t : ℝ) : ℝ :=
318 ∑ e : Fin K.nE,
319 (hingeLineSecondDeriv K hK ξ e t *
320 deficitAngle K (linePotential K ξ t) e +
321 2 * hingeLineDeriv K hK ξ e t *
322 deficitLineDeriv K ξ e t +
323 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
324 deficitLineSecondDeriv K ξ e t)
325
326/-- Product-rule target: near the flat point, the derivative of the full action
327is the finite sum of hinge-derivative and deficit-derivative terms. -/
328def ActionDerivativeProductRuleNearZeroTarget
329 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
330 ∀ ξ : VertexPotential K,
331 (fun t : ℝ => deriv (actionAlongLine K hK ξ) t) =ᶠ[nhds (0 : ℝ)]
332 fun t : ℝ => reggeActionProductRuleDerivative K hK ξ t
333
334/-- Sufficient differentiability condition for the finite product rule:
335each hinge line and each deficit line is differentiable near the flat point. -/
336def HingeDeficitLineDifferentiabilityNearZeroTarget
337 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
338 ∀ ξ : VertexPotential K,
339 ∀ᶠ t : ℝ in nhds (0 : ℝ),
340 ∀ e : Fin K.nE,
341 DifferentiableAt ℝ
342 (fun s : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ s) e) t ∧
343 DifferentiableAt ℝ
344 (fun s : ℝ => deficitAngle K (linePotential K ξ s) e) t
345
346/-- Sufficient differentiability condition for differentiating the product-rule
347expression once more at the flat point. -/
348def HingeDeficitSecondLineDifferentiabilityAtZeroTarget
349 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
350 ∀ (ξ : VertexPotential K) (e : Fin K.nE),
351 DifferentiableAt ℝ (fun t : ℝ => hingeLineDeriv K hK ξ e t) 0 ∧
352 DifferentiableAt ℝ (fun t : ℝ => deficitLineDeriv K ξ e t) 0
353
354theorem hingeLineDeriv_differentiableAt_zero
355 (K : Triangulation3D) (hK : IncidenceConsistent K)
356 (ξ : VertexPotential K) (e : Fin K.nE) :
357 DifferentiableAt ℝ (fun t : ℝ => hingeLineDeriv K hK ξ e t) 0 := by
358 unfold hingeLineDeriv hingeMeasureUnderConformal linePotential
359 let uv := K.edgeVerts e
360 let c : ℝ := (ξ uv.1 + ξ uv.2) / 2
361 have hderiv :
362 (fun t : ℝ =>
363 deriv
364 (fun s : ℝ =>
365 Real.sqrt (hK.globalSqEdge e) *
366 Real.exp ((s * ξ uv.1 + s * ξ uv.2) / 2)) t) =
367 fun t : ℝ => Real.sqrt (hK.globalSqEdge e) * c * Real.exp (t * c) := by
368 funext t
369 have hlin :
370 HasDerivAt (fun s : ℝ => (s * ξ uv.1 + s * ξ uv.2) / 2) c t := by
371 have h1 : HasDerivAt (fun s : ℝ => s * ξ uv.1) (ξ uv.1) t := by
372 simpa using (hasDerivAt_id t).mul_const (ξ uv.1)
373 have h2 : HasDerivAt (fun s : ℝ => s * ξ uv.2) (ξ uv.2) t := by
374 simpa using (hasDerivAt_id t).mul_const (ξ uv.2)
375 simpa [c, add_div] using (h1.add h2).div_const 2
376 have hexp :=
377 (Real.hasDerivAt_exp ((t * ξ uv.1 + t * ξ uv.2) / 2)).comp t hlin
378 have h' :
379 HasDerivAt
380 (fun s : ℝ =>
381 Real.sqrt (hK.globalSqEdge e) *
382 Real.exp ((s * ξ uv.1 + s * ξ uv.2) / 2))
383 (Real.sqrt (hK.globalSqEdge e) *
384 (c * Real.exp ((t * ξ uv.1 + t * ξ uv.2) / 2))) t := by
385 simpa [mul_comm, mul_left_comm, mul_assoc] using
386 hexp.const_mul (Real.sqrt (hK.globalSqEdge e))
387 rw [h'.deriv]
388 have hexp_arg : (t * ξ uv.1 + t * ξ uv.2) / 2 = t * c := by
389 simp [c]
390 ring
391 rw [hexp_arg]
392 ring
393 rw [hderiv]
394 fun_prop
395
396def DeficitSecondLineDifferentiabilityAtZeroTarget
397 (K : Triangulation3D) : Prop :=
398 ∀ (ξ : VertexPotential K) (e : Fin K.nE),
399 DifferentiableAt ℝ (fun t : ℝ => deficitLineDeriv K ξ e t) 0
400
401theorem hingeDeficitSecondLineDifferentiability_of_deficit
402 (K : Triangulation3D) (hK : IncidenceConsistent K)
403 (hDef : DeficitSecondLineDifferentiabilityAtZeroTarget K) :
404 HingeDeficitSecondLineDifferentiabilityAtZeroTarget K hK := by
405 intro ξ e
406 exact ⟨hingeLineDeriv_differentiableAt_zero K hK ξ e, hDef ξ e⟩
407
408theorem hingeLine_contDiffAt_zero
409 (K : Triangulation3D) (hK : IncidenceConsistent K)
410 (ξ : VertexPotential K) (e : Fin K.nE) :
411 ContDiffAt ℝ (⊤ : ℕ∞)
412 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e) 0 := by
413 have hline : ContDiffAt ℝ (⊤ : ℕ∞) (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
414 rw [contDiffAt_pi]
415 intro i
416 unfold linePotential
417 fun_prop
418 have hhinge : ContDiffAt ℝ (⊤ : ℕ∞)
419 (fun η : VertexPotential K => hingeMeasureUnderConformal K hK η e)
420 (linePotential K ξ 0) := by
421 simpa [linePotential_zero K ξ] using
422 ReggeActionSmoothness.hingeMeasureUnderConformal_contDiffAt_zero K hK e (⊤ : ℕ∞)
423 have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hhinge hline
424 simpa [Function.comp_def] using hcomp
425
426theorem deficitLine_contDiffAt_zero_of_flatConfiguration
427 (K : Triangulation3D) (hK : IncidenceConsistent K)
428 (hFlat : FlatConfiguration K hK)
429 (ξ : VertexPotential K) (e : Fin K.nE) :
430 ContDiffAt ℝ (⊤ : ℕ∞)
431 (fun t : ℝ => deficitAngle K (linePotential K ξ t) e) 0 := by
432 have hline : ContDiffAt ℝ (⊤ : ℕ∞) (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
433 rw [contDiffAt_pi]
434 intro i
435 unfold linePotential
436 fun_prop
437 have hdef : ContDiffAt ℝ (⊤ : ℕ∞)
438 (fun η : VertexPotential K => deficitAngle K η e)
439 (linePotential K ξ 0) := by
440 simpa [linePotential_zero K ξ] using
441 ReggeActionSmoothness.deficitAngle_contDiffAt_zero K e (⊤ : ℕ∞)
442 hFlat.local_arccos_endpoint_free
443 have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hdef hline
444 simpa [Function.comp_def] using hcomp
445
446theorem deficitLineDeriv_differentiableAt_zero_of_flatConfiguration
447 (K : Triangulation3D) (hK : IncidenceConsistent K)
448 (hFlat : FlatConfiguration K hK)
449 (ξ : VertexPotential K) (e : Fin K.nE) :
450 DifferentiableAt ℝ (fun t : ℝ => deficitLineDeriv K ξ e t) 0 := by
451 unfold deficitLineDeriv
452 exact deriv_differentiableAt_of_contDiffAt_top
453 (fun t : ℝ => deficitAngle K (linePotential K ξ t) e) 0
454 (deficitLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ e)
455
456theorem hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration
457 (K : Triangulation3D) (hK : IncidenceConsistent K)
458 (hFlat : FlatConfiguration K hK) :
459 HingeDeficitSecondLineDifferentiabilityAtZeroTarget K hK := by
460 intro ξ e
461 exact ⟨hingeLineDeriv_differentiableAt_zero K hK ξ e,
462 deficitLineDeriv_differentiableAt_zero_of_flatConfiguration K hK hFlat ξ e⟩
463
464theorem hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration
465 (K : Triangulation3D) (hK : IncidenceConsistent K)
466 (hFlat : FlatConfiguration K hK) :
467 HingeDeficitLineDifferentiabilityNearZeroTarget K hK := by
468 intro ξ
469 rw [Filter.eventually_all]
470 intro e
471 have hHinge :=
472 differentiableAt_eventually_of_contDiffAt_top
473 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e) 0
474 (hingeLine_contDiffAt_zero K hK ξ e)
475 have hDef :=
476 differentiableAt_eventually_of_contDiffAt_top
477 (fun t : ℝ => deficitAngle K (linePotential K ξ t) e) 0
478 (deficitLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ e)
479 filter_upwards [hHinge, hDef] with t htHinge htDef
480 exact ⟨htHinge, htDef⟩
481
482theorem actionDerivativeProductRuleNearZero_of_factorDifferentiability
483 (K : Triangulation3D) (hK : IncidenceConsistent K)
484 (hDiff : HingeDeficitLineDifferentiabilityNearZeroTarget K hK) :
485 ActionDerivativeProductRuleNearZeroTarget K hK := by
486 intro ξ
487 filter_upwards [hDiff ξ] with t ht
488 unfold actionAlongLine reggeAction reggeActionProductRuleDerivative
489 hingeLineDeriv deficitLineDeriv
490 have hEdge :
491 ∀ e : Fin K.nE,
492 HasDerivAt
493 (fun s : ℝ =>
494 hingeMeasureUnderConformal K hK (linePotential K ξ s) e *
495 deficitAngle K (linePotential K ξ s) e)
496 (deriv
497 (fun s : ℝ =>
498 hingeMeasureUnderConformal K hK (linePotential K ξ s) e) t *
499 deficitAngle K (linePotential K ξ t) e +
500 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
501 deriv (fun s : ℝ => deficitAngle K (linePotential K ξ s) e) t) t := by
502 intro e
503 have hL := (ht e).1.hasDerivAt
504 have hD := (ht e).2.hasDerivAt
505 simpa [mul_comm, mul_left_comm, mul_assoc] using hL.mul hD
506 have hsum :=
507 HasDerivAt.sum
508 (u := Finset.univ)
509 (A := fun e s =>
510 hingeMeasureUnderConformal K hK (linePotential K ξ s) e *
511 deficitAngle K (linePotential K ξ s) e)
512 (A' := fun e =>
513 deriv
514 (fun s : ℝ =>
515 hingeMeasureUnderConformal K hK (linePotential K ξ s) e) t *
516 deficitAngle K (linePotential K ξ t) e +
517 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
518 deriv (fun s : ℝ => deficitAngle K (linePotential K ξ s) e) t)
519 (x := t)
520 (fun e _ => hEdge e)
521 rw [show
522 (fun t : ℝ =>
523 ∑ e : Fin K.nE,
524 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
525 deficitAngle K (linePotential K ξ t) e) =
526 (∑ e : Fin K.nE,
527 fun s : ℝ =>
528 hingeMeasureUnderConformal K hK (linePotential K ξ s) e *
529 deficitAngle K (linePotential K ξ s) e) by
530 funext s
531 simp [Finset.sum_apply]]
532 simpa using hsum.deriv
533
534theorem actionDerivativeProductRuleNearZero_of_flatConfiguration
535 (K : Triangulation3D) (hK : IncidenceConsistent K)
536 (hFlat : FlatConfiguration K hK) :
537 ActionDerivativeProductRuleNearZeroTarget K hK :=
538 actionDerivativeProductRuleNearZero_of_factorDifferentiability K hK
539 (hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration K hK hFlat)
540
541theorem productRule_hasDerivAt_secondProduct
542 (K : Triangulation3D) (hK : IncidenceConsistent K)
543 (hFlat : FlatConfiguration K hK)
544 (hSecond : HingeDeficitSecondLineDifferentiabilityAtZeroTarget K hK)
545 (ξ : VertexPotential K) :
546 HasDerivAt (reggeActionProductRuleDerivative K hK ξ)
547 (reggeActionSecondProductRuleDerivative K hK ξ 0) 0 := by
548 unfold reggeActionProductRuleDerivative reggeActionSecondProductRuleDerivative
549 have hEdge :
550 ∀ e : Fin K.nE,
551 HasDerivAt
552 (fun t : ℝ =>
553 hingeLineDeriv K hK ξ e t *
554 deficitAngle K (linePotential K ξ t) e +
555 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
556 deficitLineDeriv K ξ e t)
557 (hingeLineSecondDeriv K hK ξ e 0 *
558 deficitAngle K (linePotential K ξ 0) e +
559 2 * hingeLineDeriv K hK ξ e 0 *
560 deficitLineDeriv K ξ e 0 +
561 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
562 deficitLineSecondDeriv K ξ e 0) 0 := by
563 intro e
564 have hHinge0 : DifferentiableAt ℝ
565 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e) 0 :=
566 (hingeLine_contDiffAt_zero K hK ξ e).differentiableAt (by simp)
567 have hDef0 : DifferentiableAt ℝ
568 (fun t : ℝ => deficitAngle K (linePotential K ξ t) e) 0 :=
569 (deficitLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ e).differentiableAt
570 (by simp)
571 have hHingeDeriv : HasDerivAt (fun t : ℝ => hingeLineDeriv K hK ξ e t)
572 (hingeLineSecondDeriv K hK ξ e 0) 0 := by
573 simpa [hingeLineSecondDeriv] using (hSecond ξ e).1.hasDerivAt
574 have hDefDeriv : HasDerivAt (fun t : ℝ => deficitLineDeriv K ξ e t)
575 (deficitLineSecondDeriv K ξ e 0) 0 := by
576 simpa [deficitLineSecondDeriv] using (hSecond ξ e).2.hasDerivAt
577 have hDefLine : HasDerivAt
578 (fun t : ℝ => deficitAngle K (linePotential K ξ t) e)
579 (deficitLineDeriv K ξ e 0) 0 := by
580 simpa [deficitLineDeriv] using hDef0.hasDerivAt
581 have hHingeLine : HasDerivAt
582 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e)
583 (hingeLineDeriv K hK ξ e 0) 0 := by
584 simpa [hingeLineDeriv] using hHinge0.hasDerivAt
585 have h1 := hHingeDeriv.mul hDefLine
586 have h2 := hHingeLine.mul hDefDeriv
587 have hsum := h1.add h2
588 convert hsum using 1
589 · ring
590 have hsum :=
591 HasDerivAt.sum
592 (u := Finset.univ)
593 (A := fun e t =>
594 hingeLineDeriv K hK ξ e t *
595 deficitAngle K (linePotential K ξ t) e +
596 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
597 deficitLineDeriv K ξ e t)
598 (A' := fun e =>
599 hingeLineSecondDeriv K hK ξ e 0 *
600 deficitAngle K (linePotential K ξ 0) e +
601 2 * hingeLineDeriv K hK ξ e 0 *
602 deficitLineDeriv K ξ e 0 +
603 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
604 deficitLineSecondDeriv K ξ e 0)
605 (x := 0)
606 (fun e _ => hEdge e)
607 rw [show
608 (fun t : ℝ =>
609 ∑ e : Fin K.nE,
610 (hingeLineDeriv K hK ξ e t *
611 deficitAngle K (linePotential K ξ t) e +
612 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
613 deficitLineDeriv K ξ e t)) =
614 (∑ e : Fin K.nE,
615 fun t : ℝ =>
616 hingeLineDeriv K hK ξ e t *
617 deficitAngle K (linePotential K ξ t) e +
618 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
619 deficitLineDeriv K ξ e t) by
620 funext t
621 simp [Finset.sum_apply]]
622 simpa using hsum
623
624/-- Final geometric identity after the second product rule: the second
625product-rule expression at the flat point is the canonical Hessian quadratic
626form. -/
627def SecondProductRuleEqualsCanonicalHessianTarget
628 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
629 ∀ ξ : VertexPotential K,
630 reggeActionSecondProductRuleDerivative K hK ξ 0 =
631 hessianQuadratic (canonicalReggeHessian K hK) ξ
632
633/-- Second-order Schläfli identity along a conformal line. After flatness kills
634the explicit `deficitAngle(0)` term in the second product rule, this identity
635cancels one copy of the mixed hinge/deficit derivative against the
636length-weighted second deficit derivative. -/
637def SecondSchlaefliAlongLineTarget
638 (K : Triangulation3D) (hK : IncidenceConsistent K)
639 (_hFlat : FlatConfiguration K hK) : Prop :=
640 ∀ ξ : VertexPotential K,
641 (∑ e : Fin K.nE,
642 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
643 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
644 deficitLineSecondDeriv K ξ e 0)) = 0
645
646/-- The surviving mixed term after second-order Schläfli cancellation is the
647canonical incidence Hessian quadratic form. -/
648def MixedHingeDeficitCanonicalHessianTarget
649 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
650 ∀ ξ : VertexPotential K,
651 (∑ e : Fin K.nE,
652 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0)) =
653 hessianQuadratic (canonicalReggeHessian K hK) ξ
654
655theorem hingeLineDeriv_zero_eq_directional
656 (K : Triangulation3D) (hK : IncidenceConsistent K)
657 (ξ : VertexPotential K) (e : Fin K.nE) :
658 hingeLineDeriv K hK ξ e 0 =
659 ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e := by
660 unfold hingeLineDeriv
661 have h :=
662 ReggeActionFirstVariation.hingeMeasureUnderConformal_hasDerivAt_line_zero
663 K hK ξ e
664 have h' : HasDerivAt
665 (fun s : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ s) e)
666 (ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e) 0 := by
667 convert h using 1
668 exact h'.deriv
669
670theorem deficitLineDeriv_zero_eq_deficitPackage
671 (K : Triangulation3D) (hK : IncidenceConsistent K)
672 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
673 (ξ : VertexPotential K) (e : Fin K.nE) :
674 deficitLineDeriv K ξ e 0 = D.deficitDeriv ξ e := by
675 unfold deficitLineDeriv
676 have h := D.deficit_hasDerivAt ξ e
677 have h' : HasDerivAt
678 (fun s : ℝ => deficitAngle K (linePotential K ξ s) e)
679 (D.deficitDeriv ξ e) 0 := by
680 convert h using 1
681 exact h'.deriv
682
683/-- Deficit-package form of the surviving mixed hinge/deficit target. This
684removes the opaque `deriv` wrappers from `MixedHingeDeficitCanonicalHessianTarget`
685and exposes the exact first-variation deficit derivative that must be identified
686with the canonical Hessian. -/
687def MixedHingeDeficitFromDeficitPackageTarget
688 (K : Triangulation3D) (hK : IncidenceConsistent K)
689 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK) : Prop :=
690 ∀ ξ : VertexPotential K,
691 (∑ e : Fin K.nE,
692 ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e *
693 D.deficitDeriv ξ e) =
694 hessianQuadratic (canonicalReggeHessian K hK) ξ
695
696/-- Dirichlet-energy form of the mixed target. Since the canonical Hessian
697quadratic has already been proved equal to the canonical graph Dirichlet energy,
698this is the same remaining identity with the right-hand side in energy form. -/
699def MixedHingeDeficitDirichletTarget
700 (K : Triangulation3D) (hK : IncidenceConsistent K)
701 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK) : Prop :=
702 ∀ ξ : VertexPotential K,
703 (∑ e : Fin K.nE,
704 ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e *
705 D.deficitDeriv ξ e) =
706 canonicalDirichletEnergy K hK ξ
707
708theorem mixedHingeDeficitFromDeficitPackage_of_dirichlet
709 (K : Triangulation3D) (hK : IncidenceConsistent K)
710 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
711 (hDir : MixedHingeDeficitDirichletTarget K hK D) :
712 MixedHingeDeficitFromDeficitPackageTarget K hK D := by
713 intro ξ
714 rw [hDir ξ]
715 exact (canonicalReggeHessian_quadratic_eq_dirichlet K hK ξ).symm
716
717/-- Edge-stencil form of the mixed target. This is the form meant for the
718canonical periodic Freudenthal branch, where the abstract Dirichlet energy has
719already been identified with the concrete periodic edge stencil. -/
720def MixedHingeDeficitEdgeStencilTarget
721 (K : Triangulation3D) (hK : IncidenceConsistent K)
722 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK) : Prop :=
723 ∀ ξ : VertexPotential K,
724 (∑ e : Fin K.nE,
725 ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e *
726 D.deficitDeriv ξ e) =
727 canonicalEdgeStencilDirichletEnergy K hK ξ
728
729theorem mixedHingeDeficitDirichlet_of_edgeStencil
730 (K : Triangulation3D) (hK : IncidenceConsistent K)
731 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
732 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
733 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
734 MixedHingeDeficitDirichletTarget K hK D := by
735 intro ξ
736 rw [hEdge ξ, hStencil ξ]
737
738theorem mixedHingeDeficitFromDeficitPackage_of_edgeStencil
739 (K : Triangulation3D) (hK : IncidenceConsistent K)
740 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
741 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
742 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
743 MixedHingeDeficitFromDeficitPackageTarget K hK D :=
744 mixedHingeDeficitFromDeficitPackage_of_dirichlet K hK D
745 (mixedHingeDeficitDirichlet_of_edgeStencil K hK D hEdge hStencil)
746
747theorem mixedHingeDeficitCanonicalHessian_of_deficitPackage
748 (K : Triangulation3D) (hK : IncidenceConsistent K)
749 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
750 (hMixed : MixedHingeDeficitFromDeficitPackageTarget K hK D) :
751 MixedHingeDeficitCanonicalHessianTarget K hK := by
752 intro ξ
753 calc
754 (∑ e : Fin K.nE,
755 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0))
756 = ∑ e : Fin K.nE,
757 ReggeActionFirstVariation.hingeMeasureDirectionalDeriv K hK ξ e *
758 D.deficitDeriv ξ e := by
759 refine Finset.sum_congr rfl ?_
760 intro e _
761 rw [hingeLineDeriv_zero_eq_directional K hK ξ e,
762 deficitLineDeriv_zero_eq_deficitPackage K hK D ξ e]
763 _ = hessianQuadratic (canonicalReggeHessian K hK) ξ := hMixed ξ
764
765theorem mixedHingeDeficitCanonicalHessian_of_edgeStencil
766 (K : Triangulation3D) (hK : IncidenceConsistent K)
767 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
768 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
769 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
770 MixedHingeDeficitCanonicalHessianTarget K hK :=
771 mixedHingeDeficitCanonicalHessian_of_deficitPackage K hK D
772 (mixedHingeDeficitFromDeficitPackage_of_edgeStencil K hK D hEdge hStencil)
773
774/-- Stationarity form of the second-order Schläfli target. A later local
775geometric proof should show that the weighted deficit-derivative sum is
776stationary at the flat point, e.g. by differentiating the Schläfli cancellation
777through the conformal line. -/
778def WeightedDeficitDerivativeStationaryTarget
779 (K : Triangulation3D) (hK : IncidenceConsistent K)
780 (_hFlat : FlatConfiguration K hK) : Prop :=
781 ∀ ξ : VertexPotential K,
782 HasDerivAt
783 (fun t : ℝ =>
784 ∑ e : Fin K.nE,
785 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
786 deficitLineDeriv K ξ e t)
787 0 0
788
789/-- Stronger near-flat Schläfli form: the weighted deficit-derivative sum
790vanishes in a puncture-free neighbourhood of the flat point. This is more than
791the second-order proof needs, but it is the natural target produced by a
792near-zero Schläfli cancellation theorem for the conformal line. -/
793def WeightedDeficitDerivativeEventuallyZeroTarget
794 (K : Triangulation3D) (hK : IncidenceConsistent K)
795 (_hFlat : FlatConfiguration K hK) : Prop :=
796 ∀ ξ : VertexPotential K,
797 (fun t : ℝ =>
798 ∑ e : Fin K.nE,
799 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
800 deficitLineDeriv K ξ e t) =ᶠ[nhds (0 : ℝ)]
801 fun _t : ℝ => 0
802
803theorem weightedDeficitDerivativeStationary_of_eventuallyZero
804 (K : Triangulation3D) (hK : IncidenceConsistent K)
805 (hFlat : FlatConfiguration K hK)
806 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat) :
807 WeightedDeficitDerivativeStationaryTarget K hK hFlat := by
808 intro ξ
809 have hconst : HasDerivAt (fun _t : ℝ => (0 : ℝ)) 0 0 :=
810 hasDerivAt_const 0 0
811 exact hconst.congr_of_eventuallyEq (hZero ξ)
812
813/-- Strongest geometric Schläfli form: the weighted deficit-derivative sum
814vanishes identically along the conformal line (for every parameter value, not
815just near the flat point). This is the direct consequence of the classical
816Schläfli differential identity `∑_{e ∈ τ} ℓ_e dθ_{e,τ} = 0` applied at
817every parameter `t` and summed over all tetrahedra: the per-tetrahedron
818identities cancel the `∑ h δ'` term in the Regge first variation, leaving
819`S'(t) = ∑ δ h'`, and therefore `V(t) = ∑ h δ' = 0`.
820
821Proving this target closes the full `WeightedDeficitDerivativeStationaryTarget`
822and all its downstream consumers (typed-edge targets, per-displacement-class
823targets, etc.) without any per-class decomposition. -/
824def ConformalSchlaefliAlongLineTarget
825 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
826 ∀ (ξ : VertexPotential K) (t : ℝ),
827 ∑ e : Fin K.nE,
828 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
829 deficitLineDeriv K ξ e t = 0
830
831/-- Local along-line Schläfli identity in actual derivative form. At every
832parameter `t` on a conformal line and every tetrahedron `τ`, the local
833length-weighted sum of actual dihedral-angle derivatives vanishes.
834
835This is the tetrahedral calculus content of Schläfli away from the flat point:
836it is the same identity as `local_conformal_schlaefli_cancellation`, but with
837the tetrahedron evaluated at `linePotential K ξ t` and with the actual line
838derivative `deriv (...) t` rather than the flat-point closed form. -/
839def LocalConformalSchlaefliAlongLineTarget
840 (K : Triangulation3D) : Prop :=
841 ∀ (ξ : VertexPotential K) (t : ℝ) (τ : Fin K.nT),
842 (∑ f : Fin 6,
843 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
844 deriv
845 (fun s : ℝ =>
846 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) = 0
847
848/-- Global expansion of `∑_e h_e δ'_e` into the local tetrahedral Schläfli
849sums at an arbitrary point on the conformal line.
850
851This target contains the non-flat incidence/reindexing and derivative-of-deficit
852bookkeeping:
853* expand `deficitLineDeriv` as minus the sum of actual local angle derivatives;
854* replace global hinge lengths by matching local conformal edge lengths for
855 each incident tetrahedral edge slot;
856* reindex global edge incidence to local tetrahedral edge slots. -/
857def ConformalSchlaefliAlongLineExpansionTarget
858 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
859 ∀ (ξ : VertexPotential K) (t : ℝ),
860 (∑ e : Fin K.nE,
861 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
862 deficitLineDeriv K ξ e t) =
863 - ∑ τ : Fin K.nT,
864 ∑ f : Fin 6,
865 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
866 deriv
867 (fun s : ℝ =>
868 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t
869
870/-- Local near-flat Schläfli identity along conformal lines. This is the
871right local target for the Hessian proof: it only asks for the conformal line
872near `t = 0`, where the flat nondegenerate chart supplies the intended
873tetrahedral domain. -/
874def LocalConformalSchlaefliNearZeroTarget
875 (K : Triangulation3D) : Prop :=
876 ∀ ξ : VertexPotential K,
877 ∀ᶠ t : ℝ in nhds (0 : ℝ),
878 ∀ τ : Fin K.nT,
879 (∑ f : Fin 6,
880 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
881 deriv
882 (fun s : ℝ =>
883 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) = 0
884
885/-- Non-flat local angle chain rule in squared-edge coordinates. At a nearby
886line parameter, each actual local dihedral derivative is the closed-form
887squared-edge gradient paired with the derivative of the six conformal
888squared-edge coordinates. -/
889def LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget
890 (K : Triangulation3D) : Prop :=
891 ∀ ξ : VertexPotential K,
892 ∀ᶠ t : ℝ in nhds (0 : ℝ),
893 ∀ τ : Fin K.nT, ∀ f : Fin 6,
894 deriv
895 (fun s : ℝ =>
896 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t =
897 ∑ k : Fin 6,
898 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
899 (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
900 deriv
901 (fun s : ℝ =>
902 conformalLocalSqEdge K (linePotential K ξ s) τ k) t
903
904/-- Closed-form Schläfli zero at the deformed squared-edge tuple. This is the
905algebraic non-flat identity once the conformal tetrahedron is known to remain
906inside the nondegenerate cone near `t = 0`. -/
907def LocalConformalSchlaefliClosedFormZeroNearZeroTarget
908 (K : Triangulation3D) : Prop :=
909 ∀ ξ : VertexPotential K,
910 ∀ᶠ t : ℝ in nhds (0 : ℝ),
911 ∀ τ : Fin K.nT, ∀ k : Fin 6,
912 (∑ f : Fin 6,
913 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
914 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
915 (conformalTetSqEdges K (linePotential K ξ t) τ) f k) = 0
916
917theorem conformalLocalSqEdge_line_pos
918 (K : Triangulation3D) (ξ : VertexPotential K)
919 (t : ℝ) (τ : Fin K.nT) (f : Fin 6) :
920 0 < conformalLocalSqEdge K (linePotential K ξ t) τ f := by
921 unfold conformalLocalSqEdge linePotential
922 exact mul_pos ((K.tet τ).sqEdge_pos f) (Real.exp_pos _)
923
924theorem cm3_conformalTetSqEdges_line_pos_eventually
925 (K : Triangulation3D) (ξ : VertexPotential K) (τ : Fin K.nT) :
926 ∀ᶠ t : ℝ in nhds (0 : ℝ),
927 CayleyMengerPolynomial.cm3 (conformalTetSqEdges K (linePotential K ξ t) τ) > 0 := by
928 have hline : ContDiffAt ℝ (0 : ℕ∞)
929 (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
930 rw [contDiffAt_pi]
931 intro i
932 unfold linePotential
933 fun_prop
934 have htet : ContDiffAt ℝ (0 : ℕ∞)
935 (fun η : VertexPotential K => conformalTetSqEdges K η τ)
936 (linePotential K ξ 0) := by
937 simpa [linePotential_zero K ξ] using
938 (ReggeActionSmoothness.conformalTetSqEdges_contDiff K τ (0 : ℕ∞)).contDiffAt
939 have htetLine : ContDiffAt ℝ (0 : ℕ∞)
940 (fun t : ℝ => conformalTetSqEdges K (linePotential K ξ t) τ) (0 : ℝ) := by
941 simpa [Function.comp_def] using
942 (ContDiffAt.comp (x := (0 : ℝ)) htet hline)
943 have hcm : ContinuousAt
944 (fun t : ℝ =>
945 CayleyMengerPolynomial.cm3 (conformalTetSqEdges K (linePotential K ξ t) τ))
946 (0 : ℝ) := by
947 have hbase : ContinuousAt CayleyMengerPolynomial.cm3
948 (conformalTetSqEdges K (linePotential K ξ 0) τ) :=
949 (CayleyMengerPolynomial.cm3_contDiff (0 : ℕ∞)).continuous.continuousAt
950 exact ContinuousAt.comp
951 (f := fun t : ℝ => conformalTetSqEdges K (linePotential K ξ t) τ)
952 (g := CayleyMengerPolynomial.cm3)
953 (x := (0 : ℝ))
954 hbase htetLine.continuousAt
955 have hpos0 :
956 (0 : ℝ) <
957 CayleyMengerPolynomial.cm3 (conformalTetSqEdges K (linePotential K ξ 0) τ) := by
958 simpa [linePotential_zero K ξ, ReggeActionSmoothness.conformalTetSqEdges_zero K τ]
959 using (K.tet τ).cm_pos
960 exact hcm.eventually (Ioi_mem_nhds hpos0)
961
962theorem localConformalSchlaefliClosedFormZeroNearZero
963 (K : Triangulation3D) :
964 LocalConformalSchlaefliClosedFormZeroNearZeroTarget K := by
965 intro ξ
966 rw [Filter.eventually_all]
967 intro τ
968 filter_upwards [cm3_conformalTetSqEdges_line_pos_eventually K ξ τ] with t hcm
969 intro k
970 let T : ReggeRigorousFoundation.NonDegenerateTet :=
971 { sqEdge := conformalTetSqEdges K (linePotential K ξ t) τ
972 sqEdge_pos := by
973 intro f
974 exact conformalLocalSqEdge_line_pos K ξ t τ f
975 cm_pos := hcm }
976 have hS := SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm T k
977 simpa [T, SchlaefliTetrahedronProof.dihedralClosedDerivSq, conformalTetSqEdges]
978 using hS
979
980theorem dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually
981 (K : Triangulation3D) (hK : IncidenceConsistent K)
982 (hFlat : FlatConfiguration K hK)
983 (ξ : VertexPotential K) (τ : Fin K.nT) (f : Fin 6) :
984 ∀ᶠ t : ℝ in nhds (0 : ℝ),
985 DihedralCayleyMenger.dihedralCos3Sq
986 (conformalTetSqEdges K (linePotential K ξ t) τ) f ≠ -1 ∧
987 DihedralCayleyMenger.dihedralCos3Sq
988 (conformalTetSqEdges K (linePotential K ξ t) τ) f ≠ 1 := by
989 have hline : ContDiffAt ℝ (0 : ℕ∞)
990 (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
991 rw [contDiffAt_pi]
992 intro i
993 unfold linePotential
994 fun_prop
995 have hcosEta : ContinuousAt
996 (fun η : VertexPotential K =>
997 DihedralCayleyMenger.dihedralCos3Sq (conformalTetSqEdges K η τ) f)
998 (linePotential K ξ 0) := by
999 simpa [linePotential_zero K ξ] using
1000 ReggeActionSmoothness.dihedralCos3Sq_conformal_continuousAt_zero K τ f
1001 have hcos : ContinuousAt
1002 (fun t : ℝ =>
1003 DihedralCayleyMenger.dihedralCos3Sq
1004 (conformalTetSqEdges K (linePotential K ξ t) τ) f)
1005 (0 : ℝ) :=
1006 ContinuousAt.comp
1007 (f := fun t : ℝ => linePotential K ξ t)
1008 (g := fun η : VertexPotential K =>
1009 DihedralCayleyMenger.dihedralCos3Sq (conformalTetSqEdges K η τ) f)
1010 (x := (0 : ℝ))
1011 hcosEta hline.continuousAt
1012 have hneg0 :
1013 DihedralCayleyMenger.dihedralCos3Sq
1014 (conformalTetSqEdges K (linePotential K ξ 0) τ) f ≠ -1 := by
1015 simpa [linePotential_zero K ξ, ReggeActionSmoothness.conformalTetSqEdges_zero K τ]
1016 using (hFlat.local_arccos_endpoint_free τ f).1
1017 have hpos0 :
1018 DihedralCayleyMenger.dihedralCos3Sq
1019 (conformalTetSqEdges K (linePotential K ξ 0) τ) f ≠ 1 := by
1020 simpa [linePotential_zero K ξ, ReggeActionSmoothness.conformalTetSqEdges_zero K τ]
1021 using (hFlat.local_arccos_endpoint_free τ f).2
1022 filter_upwards [hcos.eventually_ne hneg0, hcos.eventually_ne hpos0] with t hneg hpos
1023 exact ⟨hneg, hpos⟩
1024
1025theorem conformalTetSqEdges_hasDerivAt_line
1026 (K : Triangulation3D) (ξ : VertexPotential K)
1027 (t : ℝ) (τ : Fin K.nT) :
1028 HasDerivAt
1029 (fun s : ℝ => conformalTetSqEdges K (linePotential K ξ s) τ)
1030 (fun k : Fin 6 =>
1031 deriv
1032 (fun s : ℝ =>
1033 conformalLocalSqEdge K (linePotential K ξ s) τ k) t) t := by
1034 rw [hasDerivAt_pi]
1035 intro k
1036 have hdiff : DifferentiableAt ℝ
1037 (fun s : ℝ => conformalLocalSqEdge K (linePotential K ξ s) τ k) t := by
1038 unfold conformalLocalSqEdge linePotential
1039 fun_prop
1040 simpa [conformalTetSqEdges] using hdiff.hasDerivAt
1041
1042theorem localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration
1043 (K : Triangulation3D) (hK : IncidenceConsistent K)
1044 (hFlat : FlatConfiguration K hK) :
1045 LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget K := by
1046 intro ξ
1047 rw [Filter.eventually_all]
1048 intro τ
1049 rw [Filter.eventually_all]
1050 intro f
1051 filter_upwards
1052 [cm3_conformalTetSqEdges_line_pos_eventually K ξ τ,
1053 dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually K hK hFlat ξ τ f]
1054 with t hcm hEndpoint
1055 let T : ReggeRigorousFoundation.NonDegenerateTet :=
1056 { sqEdge := conformalTetSqEdges K (linePotential K ξ t) τ
1057 sqEdge_pos := by
1058 intro k
1059 exact conformalLocalSqEdge_line_pos K ξ t τ k
1060 cm_pos := hcm }
1061 let F : CayleyMengerPolynomial.SqEdges → ℝ :=
1062 fun a => DihedralDerivatives.dihedralAngle3Sq a f
1063 let v : CayleyMengerPolynomial.SqEdges :=
1064 fun k : Fin 6 =>
1065 deriv
1066 (fun s : ℝ =>
1067 conformalLocalSqEdge K (linePotential K ξ s) τ k) t
1068 have hAngle : ContDiffAt ℝ 1 F T.sqEdge := by
1069 simpa [F, T] using
1070 ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
1071 T f 1 hEndpoint
1072 have hDiff : DifferentiableAt ℝ F T.sqEdge :=
1073 hAngle.differentiableAt (by simp)
1074 have hF : HasFDerivAt F (fderiv ℝ F T.sqEdge) T.sqEdge :=
1075 hDiff.hasFDerivAt
1076 have hgamma : HasDerivAt
1077 (fun s : ℝ => conformalTetSqEdges K (linePotential K ξ s) τ) v t := by
1078 simpa [v] using conformalTetSqEdges_hasDerivAt_line K ξ t τ
1079 have hcomp := HasFDerivAt.comp_hasDerivAt
1080 (x := t)
1081 (f := fun s : ℝ => conformalTetSqEdges K (linePotential K ξ s) τ)
1082 (l := F)
1083 hF hgamma
1084 have hvalue :
1085 (fderiv ℝ F T.sqEdge) v =
1086 ∑ k : Fin 6,
1087 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
1088 (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
1089 deriv
1090 (fun s : ℝ =>
1091 conformalLocalSqEdge K (linePotential K ξ s) τ k) t := by
1092 calc
1093 (fderiv ℝ F T.sqEdge) v
1094 = ∑ k : Fin 6,
1095 v k * (fderiv ℝ F T.sqEdge)
1096 (Pi.single (M := fun _ : Fin 6 => ℝ) k (1 : ℝ)) := by
1097 exact ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single
1098 (fderiv ℝ F T.sqEdge) v
1099 _ = ∑ k : Fin 6,
1100 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
1101 (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
1102 deriv
1103 (fun s : ℝ =>
1104 conformalLocalSqEdge K (linePotential K ξ s) τ k) t := by
1105 refine Finset.sum_congr rfl ?_
1106 intro k _
1107 have hcoord :=
1108 ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
1109 T f k hEndpoint
1110 simp [F, T, v, hcoord, SchlaefliTetrahedronProof.dihedralClosedDerivSq,
1111 mul_comm]
1112 rw [hvalue] at hcomp
1113 simpa [F, Function.comp_def, tetDihedralAngleUnderConformal] using hcomp.deriv
1114
1115theorem localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero
1116 (K : Triangulation3D)
1117 (hChain : LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget K)
1118 (hZero : LocalConformalSchlaefliClosedFormZeroNearZeroTarget K) :
1119 LocalConformalSchlaefliNearZeroTarget K := by
1120 intro ξ
1121 filter_upwards [hChain ξ, hZero ξ] with t hChain_t hZero_t
1122 intro τ
1123 calc
1124 (∑ f : Fin 6,
1125 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1126 deriv
1127 (fun s : ℝ =>
1128 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t)
1129 =
1130 ∑ f : Fin 6,
1131 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1132 (∑ k : Fin 6,
1133 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
1134 (conformalTetSqEdges K (linePotential K ξ t) τ) f k *
1135 deriv
1136 (fun s : ℝ =>
1137 conformalLocalSqEdge K (linePotential K ξ s) τ k) t) := by
1138 refine Finset.sum_congr rfl ?_
1139 intro f _
1140 rw [hChain_t τ f]
1141 _ =
1142 ∑ k : Fin 6,
1143 deriv
1144 (fun s : ℝ =>
1145 conformalLocalSqEdge K (linePotential K ξ s) τ k) t *
1146 (∑ f : Fin 6,
1147 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1148 DihedralDerivatives.dihedralAngle3SqClosedFormDeriv
1149 (conformalTetSqEdges K (linePotential K ξ t) τ) f k) := by
1150 simp_rw [Finset.mul_sum]
1151 rw [Finset.sum_comm]
1152 refine Finset.sum_congr rfl ?_
1153 intro k _
1154 refine Finset.sum_congr rfl ?_
1155 intro f _
1156 ring
1157 _ = ∑ k : Fin 6,
1158 deriv
1159 (fun s : ℝ =>
1160 conformalLocalSqEdge K (linePotential K ξ s) τ k) t * 0 := by
1161 refine Finset.sum_congr rfl ?_
1162 intro k _
1163 rw [hZero_t τ k]
1164 _ = 0 := by simp
1165
1166/-- Near-flat global expansion of `∑_e h_e δ'_e` into local tetrahedral
1167Schläfli sums. This is the local-in-`t` version of
1168`ConformalSchlaefliAlongLineExpansionTarget`, and is sufficient for
1169`WeightedDeficitDerivativeEventuallyZeroTarget`. -/
1170def ConformalSchlaefliNearZeroExpansionTarget
1171 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1172 ∀ ξ : VertexPotential K,
1173 (fun t : ℝ =>
1174 ∑ e : Fin K.nE,
1175 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1176 deficitLineDeriv K ξ e t) =ᶠ[nhds (0 : ℝ)]
1177 (fun t : ℝ =>
1178 - ∑ τ : Fin K.nT,
1179 ∑ f : Fin 6,
1180 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1181 deriv
1182 (fun s : ℝ =>
1183 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t)
1184
1185/-- Local dihedral-angle line differentiability near the flat point. This is
1186the analytic input needed to expand the derivative of a deficit angle into the
1187finite sum of derivatives of its incident local dihedral angles. -/
1188def LocalDihedralAngleLineDifferentiabilityNearZeroTarget
1189 (K : Triangulation3D) : Prop :=
1190 ∀ ξ : VertexPotential K,
1191 ∀ᶠ t : ℝ in nhds (0 : ℝ),
1192 ∀ τ : Fin K.nT, ∀ f : Fin 6,
1193 DifferentiableAt ℝ
1194 (fun s : ℝ =>
1195 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t
1196
1197theorem tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration
1198 (K : Triangulation3D) (hK : IncidenceConsistent K)
1199 (hFlat : FlatConfiguration K hK)
1200 (ξ : VertexPotential K) (τ : Fin K.nT) (f : Fin 6) :
1201 ContDiffAt ℝ (⊤ : ℕ∞)
1202 (fun t : ℝ =>
1203 tetDihedralAngleUnderConformal K (linePotential K ξ t) τ f) 0 := by
1204 have hline : ContDiffAt ℝ (⊤ : ℕ∞) (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
1205 rw [contDiffAt_pi]
1206 intro i
1207 unfold linePotential
1208 fun_prop
1209 have hangle : ContDiffAt ℝ (⊤ : ℕ∞)
1210 (fun η : VertexPotential K => tetDihedralAngleUnderConformal K η τ f)
1211 (linePotential K ξ 0) := by
1212 simpa [linePotential_zero K ξ] using
1213 ReggeActionSmoothness.tetDihedralAngleUnderConformal_contDiffAt_zero
1214 K τ f (⊤ : ℕ∞) (hFlat.local_arccos_endpoint_free τ f)
1215 have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hangle hline
1216 simpa [Function.comp_def] using hcomp
1217
1218theorem localDihedralAngleLineDifferentiabilityNearZero_of_flatConfiguration
1219 (K : Triangulation3D) (hK : IncidenceConsistent K)
1220 (hFlat : FlatConfiguration K hK) :
1221 LocalDihedralAngleLineDifferentiabilityNearZeroTarget K := by
1222 intro ξ
1223 rw [Filter.eventually_all]
1224 intro τ
1225 rw [Filter.eventually_all]
1226 intro f
1227 exact differentiableAt_eventually_of_contDiffAt_top
1228 (fun t : ℝ => tetDihedralAngleUnderConformal K (linePotential K ξ t) τ f)
1229 0
1230 (tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration
1231 K hK hFlat ξ τ f)
1232
1233theorem hingeMeasureUnderConformal_eq_local_sqrt_of_incident
1234 (K : Triangulation3D) (hK : IncidenceConsistent K)
1235 (ξ : VertexPotential K) (e : Fin K.nE) (τ : Fin K.nT) (f : Fin 6)
1236 (h : K.edgeInTet e τ = some f) :
1237 hingeMeasureUnderConformal K hK ξ e =
1238 Real.sqrt (conformalLocalSqEdge K ξ τ f) := by
1239 unfold hingeMeasureUnderConformal conformalLocalSqEdge
1240 let ev := K.edgeVerts e
1241 let fv := ReggeRigorousFoundation.edgeVertices f
1242 have hsq : (K.tet τ).sqEdge f = hK.globalSqEdge e :=
1243 hK.local_sqEdge_eq_global e τ f h
1244 have hverts := hK.edgeInTet_vertices e τ f h
1245 have hexp_arg :
1246 ξ (K.tetVerts τ fv.1) + ξ (K.tetVerts τ fv.2) =
1247 ξ ev.1 + ξ ev.2 := by
1248 dsimp [ev, fv] at hverts ⊢
1249 rcases hverts with hdir | hrev
1250 · rw [hdir.1, hdir.2]
1251 · rw [hrev.1, hrev.2]
1252 ring
1253 rw [hsq]
1254 change Real.sqrt (hK.globalSqEdge e) * Real.exp ((ξ ev.1 + ξ ev.2) / 2) =
1255 Real.sqrt
1256 (hK.globalSqEdge e *
1257 Real.exp (ξ (K.tetVerts τ fv.1) + ξ (K.tetVerts τ fv.2)))
1258 rw [hexp_arg]
1259 have hglobal_nonneg : 0 ≤ hK.globalSqEdge e := by
1260 rw [← hsq]
1261 exact le_of_lt ((K.tet τ).sqEdge_pos f)
1262 rw [Real.sqrt_mul hglobal_nonneg]
1263 have hsqrt_exp :
1264 Real.sqrt (Real.exp (ξ ev.1 + ξ ev.2)) =
1265 Real.exp ((ξ ev.1 + ξ ev.2) / 2) := by
1266 have hsquare :
1267 Real.exp (ξ ev.1 + ξ ev.2) =
1268 (Real.exp ((ξ ev.1 + ξ ev.2) / 2)) ^ (2 : ℕ) := by
1269 have hadd :
1270 (ξ ev.1 + ξ ev.2) / 2 + (ξ ev.1 + ξ ev.2) / 2 =
1271 ξ ev.1 + ξ ev.2 := by
1272 ring
1273 rw [pow_two, ← Real.exp_add]
1274 rw [hadd]
1275 rw [hsquare, Real.sqrt_sq_eq_abs]
1276 exact abs_of_pos (Real.exp_pos _)
1277 rw [hsqrt_exp]
1278
1279theorem incidenceEdgeSlotPartition_edge_sum_for_tet_conformal
1280 {K : Triangulation3D} {hK : IncidenceConsistent K}
1281 (P : ReggeActionFirstVariation.IncidenceEdgeSlotPartition K hK)
1282 (ξ : VertexPotential K)
1283 (w : Fin K.nT → Fin 6 → ℝ) (τ : Fin K.nT) :
1284 (∑ e : Fin K.nE,
1285 hingeMeasureUnderConformal K hK ξ e *
1286 (match K.edgeInTet e τ with
1287 | none => 0
1288 | some f => w τ f)) =
1289 ∑ f : Fin 6, Real.sqrt (conformalLocalSqEdge K ξ τ f) * w τ f := by
1290 calc
1291 (∑ e : Fin K.nE,
1292 hingeMeasureUnderConformal K hK ξ e *
1293 (match K.edgeInTet e τ with
1294 | none => 0
1295 | some f => w τ f))
1296 =
1297 ∑ e : Fin K.nE,
1298 ∑ f : Fin 6,
1299 if K.edgeInTet e τ = some f then
1300 hingeMeasureUnderConformal K hK ξ e * w τ f
1301 else 0 := by
1302 refine Finset.sum_congr rfl ?_
1303 intro e _
1304 cases h : K.edgeInTet e τ with
1305 | none =>
1306 simp
1307 | some f0 =>
1308 simp
1309 _ = ∑ f : Fin 6,
1310 ∑ e : Fin K.nE,
1311 if K.edgeInTet e τ = some f then
1312 hingeMeasureUnderConformal K hK ξ e * w τ f
1313 else 0 := by
1314 rw [Finset.sum_comm]
1315 _ = ∑ f : Fin 6,
1316 hingeMeasureUnderConformal K hK ξ (P.localEdgeOf τ f) * w τ f := by
1317 refine Finset.sum_congr rfl ?_
1318 intro f _
1319 have hsum := Finset.sum_eq_single
1320 (s := Finset.univ)
1321 (f := fun e : Fin K.nE =>
1322 (if K.edgeInTet e τ = some f then
1323 hingeMeasureUnderConformal K hK ξ e * w τ f
1324 else 0 : ℝ))
1325 (P.localEdgeOf τ f) ?_ ?_
1326 · simpa [P.localEdgeOf_incident τ f] using hsum
1327 · intro e _ he_ne
1328 have hnot : K.edgeInTet e τ ≠ some f := by
1329 intro h
1330 exact he_ne ((P.edgeInTet_iff e τ f).1 h)
1331 simp [hnot]
1332 · intro hnot_mem
1333 exact (hnot_mem (Finset.mem_univ _)).elim
1334 _ = ∑ f : Fin 6, Real.sqrt (conformalLocalSqEdge K ξ τ f) * w τ f := by
1335 refine Finset.sum_congr rfl ?_
1336 intro f _
1337 rw [hingeMeasureUnderConformal_eq_local_sqrt_of_incident
1338 K hK ξ (P.localEdgeOf τ f) τ f (P.localEdgeOf_incident τ f)]
1339
1340theorem incidenceEdgeSlotPartition_sum_match_conformal
1341 {K : Triangulation3D} {hK : IncidenceConsistent K}
1342 (P : ReggeActionFirstVariation.IncidenceEdgeSlotPartition K hK)
1343 (ξ : VertexPotential K)
1344 (w : Fin K.nT → Fin 6 → ℝ) :
1345 (∑ e : Fin K.nE,
1346 hingeMeasureUnderConformal K hK ξ e *
1347 (∑ τ : Fin K.nT,
1348 match K.edgeInTet e τ with
1349 | none => 0
1350 | some f => w τ f)) =
1351 ∑ τ : Fin K.nT,
1352 ∑ f : Fin 6,
1353 Real.sqrt (conformalLocalSqEdge K ξ τ f) * w τ f := by
1354 calc
1355 (∑ e : Fin K.nE,
1356 hingeMeasureUnderConformal K hK ξ e *
1357 (∑ τ : Fin K.nT,
1358 match K.edgeInTet e τ with
1359 | none => 0
1360 | some f => w τ f))
1361 =
1362 ∑ e : Fin K.nE,
1363 ∑ τ : Fin K.nT,
1364 hingeMeasureUnderConformal K hK ξ e *
1365 (match K.edgeInTet e τ with
1366 | none => 0
1367 | some f => w τ f) := by
1368 refine Finset.sum_congr rfl ?_
1369 intro e _
1370 rw [Finset.mul_sum]
1371 _ = ∑ τ : Fin K.nT,
1372 ∑ e : Fin K.nE,
1373 hingeMeasureUnderConformal K hK ξ e *
1374 (match K.edgeInTet e τ with
1375 | none => 0
1376 | some f => w τ f) := by
1377 rw [Finset.sum_comm]
1378 _ = ∑ τ : Fin K.nT,
1379 ∑ f : Fin 6,
1380 Real.sqrt (conformalLocalSqEdge K ξ τ f) * w τ f := by
1381 refine Finset.sum_congr rfl ?_
1382 intro τ _
1383 exact incidenceEdgeSlotPartition_edge_sum_for_tet_conformal P ξ w τ
1384
1385theorem deficitLineDeriv_eq_neg_sum_local_nearZero
1386 (K : Triangulation3D)
1387 (hDiff : LocalDihedralAngleLineDifferentiabilityNearZeroTarget K)
1388 (ξ : VertexPotential K) :
1389 ∀ᶠ t : ℝ in nhds (0 : ℝ),
1390 ∀ e : Fin K.nE,
1391 deficitLineDeriv K ξ e t =
1392 - ∑ τ : Fin K.nT,
1393 match K.edgeInTet e τ with
1394 | none => 0
1395 | some f =>
1396 deriv
1397 (fun s : ℝ =>
1398 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t := by
1399 filter_upwards [hDiff ξ] with t ht e
1400 unfold deficitLineDeriv deficitAngle localDeficitAngleContribution
1401 have hlocal :
1402 ∀ τ : Fin K.nT,
1403 HasDerivAt
1404 (fun s : ℝ =>
1405 match K.edgeInTet e τ with
1406 | none => 0
1407 | some f =>
1408 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f)
1409 (match K.edgeInTet e τ with
1410 | none => 0
1411 | some f =>
1412 deriv
1413 (fun s : ℝ =>
1414 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) t := by
1415 intro τ
1416 cases h : K.edgeInTet e τ with
1417 | none =>
1418 simpa [h] using (hasDerivAt_const t (0 : ℝ))
1419 | some f =>
1420 simpa [h] using (ht τ f).hasDerivAt
1421 have hsum : HasDerivAt
1422 (fun s : ℝ =>
1423 ∑ τ : Fin K.nT,
1424 match K.edgeInTet e τ with
1425 | none => 0
1426 | some f =>
1427 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f)
1428 (∑ τ : Fin K.nT,
1429 match K.edgeInTet e τ with
1430 | none => 0
1431 | some f =>
1432 deriv
1433 (fun s : ℝ =>
1434 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) t := by
1435 have hsum' :=
1436 HasDerivAt.sum
1437 (u := Finset.univ)
1438 (A := fun τ s =>
1439 match K.edgeInTet e τ with
1440 | none => 0
1441 | some f =>
1442 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f)
1443 (A' := fun τ =>
1444 match K.edgeInTet e τ with
1445 | none => 0
1446 | some f =>
1447 deriv
1448 (fun s : ℝ =>
1449 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t)
1450 (x := t)
1451 (fun τ _ => hlocal τ)
1452 convert hsum' using 1
1453 ext s
1454 simp [Finset.sum_apply]
1455 have hconst : HasDerivAt (fun _s : ℝ => 2 * Real.pi) 0 t :=
1456 hasDerivAt_const t (2 * Real.pi)
1457 have hderiv := hconst.sub hsum
1458 have hfun :
1459 (fun s : ℝ =>
1460 2 * Real.pi -
1461 ∑ τ : Fin K.nT,
1462 match K.edgeInTet e τ with
1463 | some f =>
1464 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f
1465 | none => 0) =
1466 ((fun _s : ℝ => 2 * Real.pi) -
1467 fun s : ℝ =>
1468 ∑ τ : Fin K.nT,
1469 match K.edgeInTet e τ with
1470 | none => 0
1471 | some f =>
1472 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) := by
1473 funext s
1474 have hsum_match :
1475 (∑ τ : Fin K.nT,
1476 match K.edgeInTet e τ with
1477 | some f =>
1478 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f
1479 | none => 0) =
1480 ∑ τ : Fin K.nT,
1481 match K.edgeInTet e τ with
1482 | none => 0
1483 | some f =>
1484 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f := by
1485 refine Finset.sum_congr rfl ?_
1486 intro τ _
1487 cases K.edgeInTet e τ <;> rfl
1488 simp [Pi.sub_apply, hsum_match]
1489 have hleft_has : HasDerivAt
1490 (fun s : ℝ =>
1491 2 * Real.pi -
1492 ∑ τ : Fin K.nT,
1493 match K.edgeInTet e τ with
1494 | some f =>
1495 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f
1496 | none => 0)
1497 (-∑ τ : Fin K.nT,
1498 match K.edgeInTet e τ with
1499 | none => 0
1500 | some f =>
1501 deriv
1502 (fun s : ℝ =>
1503 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) t := by
1504 rw [hfun]
1505 simpa [Pi.sub_apply] using hderiv
1506 simpa [mul_comm] using hleft_has.deriv
1507
1508theorem conformalSchlaefliNearZeroExpansion_of_angleDiff_and_partition
1509 (K : Triangulation3D) (hK : IncidenceConsistent K)
1510 (P : ReggeActionFirstVariation.IncidenceEdgeSlotPartition K hK)
1511 (hDiff : LocalDihedralAngleLineDifferentiabilityNearZeroTarget K) :
1512 ConformalSchlaefliNearZeroExpansionTarget K hK := by
1513 intro ξ
1514 filter_upwards [deficitLineDeriv_eq_neg_sum_local_nearZero K hDiff ξ] with t ht
1515 calc
1516 (∑ e : Fin K.nE,
1517 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1518 deficitLineDeriv K ξ e t)
1519 =
1520 ∑ e : Fin K.nE,
1521 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1522 (-∑ τ : Fin K.nT,
1523 match K.edgeInTet e τ with
1524 | none => 0
1525 | some f =>
1526 deriv
1527 (fun s : ℝ =>
1528 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) := by
1529 refine Finset.sum_congr rfl ?_
1530 intro e _
1531 rw [ht e]
1532 _ =
1533 - (∑ e : Fin K.nE,
1534 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1535 (∑ τ : Fin K.nT,
1536 match K.edgeInTet e τ with
1537 | none => 0
1538 | some f =>
1539 deriv
1540 (fun s : ℝ =>
1541 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t)) := by
1542 rw [← Finset.sum_neg_distrib]
1543 refine Finset.sum_congr rfl ?_
1544 intro e _
1545 ring
1546 _ =
1547 - ∑ τ : Fin K.nT,
1548 ∑ f : Fin 6,
1549 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1550 deriv
1551 (fun s : ℝ =>
1552 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t := by
1553 rw [incidenceEdgeSlotPartition_sum_match_conformal P (linePotential K ξ t)
1554 (fun τ f =>
1555 deriv
1556 (fun s : ℝ =>
1557 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t)]
1558
1559theorem weightedDeficitDerivativeEventuallyZero_of_nearZeroExpansion_and_local
1560 (K : Triangulation3D) (hK : IncidenceConsistent K)
1561 (hFlat : FlatConfiguration K hK)
1562 (hExpand : ConformalSchlaefliNearZeroExpansionTarget K hK)
1563 (hLocal : LocalConformalSchlaefliNearZeroTarget K) :
1564 WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat := by
1565 intro ξ
1566 filter_upwards [hExpand ξ, hLocal ξ] with t hExpand_t hLocal_t
1567 rw [hExpand_t]
1568 have hτ : ∀ τ : Fin K.nT,
1569 (∑ f : Fin 6,
1570 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1571 deriv
1572 (fun s : ℝ =>
1573 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) = 0 := by
1574 intro τ
1575 exact hLocal_t τ
1576 simp_rw [hτ]
1577 simp
1578
1579theorem weightedDeficitDerivativeStationary_of_nearZeroExpansion_and_local
1580 (K : Triangulation3D) (hK : IncidenceConsistent K)
1581 (hFlat : FlatConfiguration K hK)
1582 (hExpand : ConformalSchlaefliNearZeroExpansionTarget K hK)
1583 (hLocal : LocalConformalSchlaefliNearZeroTarget K) :
1584 WeightedDeficitDerivativeStationaryTarget K hK hFlat :=
1585 weightedDeficitDerivativeStationary_of_eventuallyZero K hK hFlat
1586 (weightedDeficitDerivativeEventuallyZero_of_nearZeroExpansion_and_local
1587 K hK hFlat hExpand hLocal)
1588
1589theorem conformalSchlaefliAlongLine_of_expansion_and_local
1590 (K : Triangulation3D) (hK : IncidenceConsistent K)
1591 (hExpand : ConformalSchlaefliAlongLineExpansionTarget K hK)
1592 (hLocal : LocalConformalSchlaefliAlongLineTarget K) :
1593 ConformalSchlaefliAlongLineTarget K hK := by
1594 intro ξ t
1595 rw [hExpand ξ t]
1596 have hτ : ∀ τ : Fin K.nT,
1597 (∑ f : Fin 6,
1598 Real.sqrt (conformalLocalSqEdge K (linePotential K ξ t) τ f) *
1599 deriv
1600 (fun s : ℝ =>
1601 tetDihedralAngleUnderConformal K (linePotential K ξ s) τ f) t) = 0 := by
1602 intro τ
1603 exact hLocal ξ t τ
1604 simp_rw [hτ]
1605 simp
1606
1607theorem weightedDeficitDerivativeEventuallyZero_of_conformalSchlaefliAlongLine
1608 (K : Triangulation3D) (hK : IncidenceConsistent K)
1609 (hFlat : FlatConfiguration K hK)
1610 (hSchlaefli : ConformalSchlaefliAlongLineTarget K hK) :
1611 WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat := by
1612 intro ξ
1613 have h_eq : (fun t : ℝ =>
1614 ∑ e : Fin K.nE,
1615 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1616 deficitLineDeriv K ξ e t) = fun _t : ℝ => 0 := by
1617 funext t
1618 exact hSchlaefli ξ t
1619 simp only [h_eq, Filter.eventuallyEq_iff_exists_mem]
1620 exact ⟨Set.univ, Filter.univ_mem, fun _ _ => rfl⟩
1621
1622theorem weightedDeficitDerivativeStationary_of_conformalSchlaefliAlongLine
1623 (K : Triangulation3D) (hK : IncidenceConsistent K)
1624 (hFlat : FlatConfiguration K hK)
1625 (hSchlaefli : ConformalSchlaefliAlongLineTarget K hK) :
1626 WeightedDeficitDerivativeStationaryTarget K hK hFlat :=
1627 weightedDeficitDerivativeStationary_of_eventuallyZero K hK hFlat
1628 (weightedDeficitDerivativeEventuallyZero_of_conformalSchlaefliAlongLine
1629 K hK hFlat hSchlaefli)
1630
1631theorem weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum
1632 (K : Triangulation3D) (hK : IncidenceConsistent K)
1633 (hFlat : FlatConfiguration K hK)
1634 (ξ : VertexPotential K) :
1635 HasDerivAt
1636 (fun t : ℝ =>
1637 ∑ e : Fin K.nE,
1638 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1639 deficitLineDeriv K ξ e t)
1640 (∑ e : Fin K.nE,
1641 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1642 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1643 deficitLineSecondDeriv K ξ e 0)) 0 := by
1644 have hSecond :=
1645 hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration K hK hFlat
1646 have hEdge : ∀ e : Fin K.nE,
1647 HasDerivAt
1648 (fun t : ℝ =>
1649 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1650 deficitLineDeriv K ξ e t)
1651 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1652 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1653 deficitLineSecondDeriv K ξ e 0) 0 := by
1654 intro e
1655 have hHinge0 : DifferentiableAt ℝ
1656 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e) 0 :=
1657 (hingeLine_contDiffAt_zero K hK ξ e).differentiableAt (by simp)
1658 have hHingeLine : HasDerivAt
1659 (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e)
1660 (hingeLineDeriv K hK ξ e 0) 0 := by
1661 simpa [hingeLineDeriv] using hHinge0.hasDerivAt
1662 have hDefDeriv : HasDerivAt (fun t : ℝ => deficitLineDeriv K ξ e t)
1663 (deficitLineSecondDeriv K ξ e 0) 0 := by
1664 simpa [deficitLineSecondDeriv] using (hSecond ξ e).2.hasDerivAt
1665 simpa [mul_comm, mul_left_comm, mul_assoc] using hHingeLine.mul hDefDeriv
1666 have hsum := HasDerivAt.sum
1667 (u := Finset.univ)
1668 (A := fun e t => hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1669 deficitLineDeriv K ξ e t)
1670 (A' := fun e => hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1671 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1672 deficitLineSecondDeriv K ξ e 0)
1673 (x := 0)
1674 (fun e _ => hEdge e)
1675 rw [show
1676 (fun t : ℝ =>
1677 ∑ e : Fin K.nE,
1678 hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1679 deficitLineDeriv K ξ e t) =
1680 (∑ e : Fin K.nE,
1681 fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e *
1682 deficitLineDeriv K ξ e t) by
1683 funext t
1684 simp [Finset.sum_apply]]
1685 simpa using hsum
1686
1687theorem secondSchlaefliAlongLine_of_weightedStationary
1688 (K : Triangulation3D) (hK : IncidenceConsistent K)
1689 (hFlat : FlatConfiguration K hK)
1690 (hStat : WeightedDeficitDerivativeStationaryTarget K hK hFlat) :
1691 SecondSchlaefliAlongLineTarget K hK hFlat := by
1692 intro ξ
1693 have hcalc := weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum K hK hFlat ξ
1694 have hzero := hcalc.unique (hStat ξ)
1695 simpa using hzero
1696
1697theorem weightedDeficitDerivativeStationary_of_secondSchlaefliAlongLine
1698 (K : Triangulation3D) (hK : IncidenceConsistent K)
1699 (hFlat : FlatConfiguration K hK)
1700 (hSch : SecondSchlaefliAlongLineTarget K hK hFlat) :
1701 WeightedDeficitDerivativeStationaryTarget K hK hFlat := by
1702 intro ξ
1703 have hcalc := weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum K hK hFlat ξ
1704 rw [hSch ξ] at hcalc
1705 exact hcalc
1706
1707theorem weightedDeficitDerivativeStationaryTarget_iff_secondSchlaefliAlongLine
1708 (K : Triangulation3D) (hK : IncidenceConsistent K)
1709 (hFlat : FlatConfiguration K hK) :
1710 WeightedDeficitDerivativeStationaryTarget K hK hFlat ↔
1711 SecondSchlaefliAlongLineTarget K hK hFlat :=
1712 ⟨secondSchlaefliAlongLine_of_weightedStationary K hK hFlat,
1713 weightedDeficitDerivativeStationary_of_secondSchlaefliAlongLine K hK hFlat⟩
1714
1715theorem secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed
1716 (K : Triangulation3D) (hK : IncidenceConsistent K)
1717 (hFlat : FlatConfiguration K hK)
1718 (hSch : SecondSchlaefliAlongLineTarget K hK hFlat)
1719 (hMixed : MixedHingeDeficitCanonicalHessianTarget K hK) :
1720 SecondProductRuleEqualsCanonicalHessianTarget K hK := by
1721 intro ξ
1722 have hzero : ∀ e : Fin K.nE,
1723 deficitAngle K (linePotential K ξ 0) e = 0 := by
1724 intro e
1725 simpa [linePotential_zero K ξ] using hFlat.flat_deficit_zero e
1726 have hsplit :
1727 reggeActionSecondProductRuleDerivative K hK ξ 0 =
1728 (∑ e : Fin K.nE,
1729 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0)) +
1730 (∑ e : Fin K.nE,
1731 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1732 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1733 deficitLineSecondDeriv K ξ e 0)) := by
1734 unfold reggeActionSecondProductRuleDerivative
1735 calc
1736 (∑ e : Fin K.nE,
1737 (hingeLineSecondDeriv K hK ξ e 0 *
1738 deficitAngle K (linePotential K ξ 0) e +
1739 2 * hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1740 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1741 deficitLineSecondDeriv K ξ e 0))
1742 = ∑ e : Fin K.nE,
1743 (0 + 2 * hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1744 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1745 deficitLineSecondDeriv K ξ e 0) := by
1746 refine Finset.sum_congr rfl ?_
1747 intro e _
1748 rw [hzero e]
1749 ring
1750 _ = ∑ e : Fin K.nE,
1751 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1752 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1753 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1754 deficitLineSecondDeriv K ξ e 0)) := by
1755 refine Finset.sum_congr rfl ?_
1756 intro e _
1757 ring
1758 _ = (∑ e : Fin K.nE,
1759 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0)) +
1760 (∑ e : Fin K.nE,
1761 (hingeLineDeriv K hK ξ e 0 * deficitLineDeriv K ξ e 0 +
1762 hingeMeasureUnderConformal K hK (linePotential K ξ 0) e *
1763 deficitLineSecondDeriv K ξ e 0)) := by
1764 rw [Finset.sum_add_distrib]
1765 rw [hsplit, hSch ξ, hMixed ξ]
1766 ring
1767
1768theorem secondProductRuleEqualsCanonicalHessian_of_eventuallyZero_and_edgeStencil
1769 (K : Triangulation3D) (hK : IncidenceConsistent K)
1770 (hFlat : FlatConfiguration K hK)
1771 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1772 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
1773 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1774 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1775 SecondProductRuleEqualsCanonicalHessianTarget K hK :=
1776 secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed K hK hFlat
1777 (secondSchlaefliAlongLine_of_weightedStationary K hK hFlat
1778 (weightedDeficitDerivativeStationary_of_eventuallyZero K hK hFlat hZero))
1779 (mixedHingeDeficitCanonicalHessian_of_edgeStencil K hK D hEdge hStencil)
1780
1781theorem secondProductRuleEqualsCanonicalHessian_of_weightedStationary_and_edgeStencil
1782 (K : Triangulation3D) (hK : IncidenceConsistent K)
1783 (hFlat : FlatConfiguration K hK)
1784 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1785 (hStat : WeightedDeficitDerivativeStationaryTarget K hK hFlat)
1786 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1787 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1788 SecondProductRuleEqualsCanonicalHessianTarget K hK :=
1789 secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed K hK hFlat
1790 (secondSchlaefliAlongLine_of_weightedStationary K hK hFlat hStat)
1791 (mixedHingeDeficitCanonicalHessian_of_edgeStencil K hK D hEdge hStencil)
1792
1793/-- Equivalent final geometric derivative target: the product-rule expression
1794itself has the canonical Hessian as its derivative at the flat point. -/
1795def ProductRuleDerivativeCanonicalHessianTarget
1796 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1797 ∀ ξ : VertexPotential K,
1798 HasDerivAt (reggeActionProductRuleDerivative K hK ξ)
1799 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0
1800
1801theorem productRuleDerivativeCanonicalHessian_of_secondProduct
1802 (K : Triangulation3D) (hK : IncidenceConsistent K)
1803 (hFlat : FlatConfiguration K hK)
1804 (hSecond : HingeDeficitSecondLineDifferentiabilityAtZeroTarget K hK)
1805 (hGeom : SecondProductRuleEqualsCanonicalHessianTarget K hK) :
1806 ProductRuleDerivativeCanonicalHessianTarget K hK := by
1807 intro ξ
1808 rw [← hGeom ξ]
1809 exact productRule_hasDerivAt_secondProduct K hK hFlat hSecond ξ
1810
1811theorem productRuleDerivativeCanonicalHessian_of_flat_secondProduct
1812 (K : Triangulation3D) (hK : IncidenceConsistent K)
1813 (hFlat : FlatConfiguration K hK)
1814 (hGeom : SecondProductRuleEqualsCanonicalHessianTarget K hK) :
1815 ProductRuleDerivativeCanonicalHessianTarget K hK :=
1816 productRuleDerivativeCanonicalHessian_of_secondProduct K hK hFlat
1817 (hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration K hK hFlat)
1818 hGeom
1819
1820theorem productRuleDerivativeCanonicalHessian_of_eventuallyZero_and_edgeStencil
1821 (K : Triangulation3D) (hK : IncidenceConsistent K)
1822 (hFlat : FlatConfiguration K hK)
1823 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1824 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
1825 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1826 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1827 ProductRuleDerivativeCanonicalHessianTarget K hK :=
1828 productRuleDerivativeCanonicalHessian_of_flat_secondProduct K hK hFlat
1829 (secondProductRuleEqualsCanonicalHessian_of_eventuallyZero_and_edgeStencil
1830 K hK hFlat D hZero hEdge hStencil)
1831
1832theorem productRuleDerivativeCanonicalHessian_of_weightedStationary_and_edgeStencil
1833 (K : Triangulation3D) (hK : IncidenceConsistent K)
1834 (hFlat : FlatConfiguration K hK)
1835 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1836 (hStat : WeightedDeficitDerivativeStationaryTarget K hK hFlat)
1837 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1838 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1839 ProductRuleDerivativeCanonicalHessianTarget K hK :=
1840 productRuleDerivativeCanonicalHessian_of_flat_secondProduct K hK hFlat
1841 (secondProductRuleEqualsCanonicalHessian_of_weightedStationary_and_edgeStencil
1842 K hK hFlat D hStat hEdge hStencil)
1843
1844/-- After the product-rule expression is available, the remaining geometric
1845linearization is that expression's first-order tangency to the canonical
1846quadratic-line derivative. -/
1847def ProductRuleTangencyToQuadraticTarget
1848 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1849 ∀ ξ : VertexPotential K,
1850 HasDerivAt
1851 (fun t : ℝ =>
1852 reggeActionProductRuleDerivative K hK ξ t -
1853 deriv (canonicalQuadraticAlongLine K hK ξ) t)
1854 0 0
1855
1856theorem productRuleTangencyToQuadratic_of_productRuleDerivativeCanonicalHessian
1857 (K : Triangulation3D) (hK : IncidenceConsistent K)
1858 (hProdDeriv : ProductRuleDerivativeCanonicalHessianTarget K hK) :
1859 ProductRuleTangencyToQuadraticTarget K hK := by
1860 intro ξ
1861 have hQuad := canonicalQuadraticAlongLine_hasSecondDerivAt_zero K hK ξ
1862 have hsub := (hProdDeriv ξ).sub hQuad
1863 have hzero :
1864 hessianQuadratic (canonicalReggeHessian K hK) ξ -
1865 hessianQuadratic (canonicalReggeHessian K hK) ξ = 0 := by
1866 ring
1867 simpa [Pi.sub_apply, hzero] using hsub
1868
1869theorem actionDerivativeTangencyToQuadratic_of_productRule
1870 (K : Triangulation3D) (hK : IncidenceConsistent K)
1871 (hProd : ActionDerivativeProductRuleNearZeroTarget K hK)
1872 (hTan : ProductRuleTangencyToQuadraticTarget K hK) :
1873 ActionDerivativeTangencyToQuadraticTarget K hK := by
1874 intro ξ
1875 refine (hTan ξ).congr_of_eventuallyEq ?_
1876 filter_upwards [hProd ξ] with t ht
1877 rw [ht]
1878
1879theorem actionDerivativeTangencyToQuadratic_of_flat_productRuleDerivativeCanonicalHessian
1880 (K : Triangulation3D) (hK : IncidenceConsistent K)
1881 (hFlat : FlatConfiguration K hK)
1882 (hProdDeriv : ProductRuleDerivativeCanonicalHessianTarget K hK) :
1883 ActionDerivativeTangencyToQuadraticTarget K hK :=
1884 actionDerivativeTangencyToQuadratic_of_productRule K hK
1885 (actionDerivativeProductRuleNearZero_of_flatConfiguration K hK hFlat)
1886 (productRuleTangencyToQuadratic_of_productRuleDerivativeCanonicalHessian K hK hProdDeriv)
1887
1888theorem nonlinearDirectionalHessian_of_actionDerivativeTangencyToQuadratic
1889 (K : Triangulation3D) (hK : IncidenceConsistent K)
1890 (hTan : ActionDerivativeTangencyToQuadraticTarget K hK) :
1891 NonlinearReggeDirectionalHessianTheorem K hK :=
1892 nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency K hK
1893 (actionDerivativeFirstOrderTangency_of_quadraticTangency K hK hTan)
1894
1895theorem actionDerivativeTangencyToQuadratic_of_eventuallyZero_and_edgeStencil
1896 (K : Triangulation3D) (hK : IncidenceConsistent K)
1897 (hFlat : FlatConfiguration K hK)
1898 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1899 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
1900 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1901 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1902 ActionDerivativeTangencyToQuadraticTarget K hK :=
1903 actionDerivativeTangencyToQuadratic_of_flat_productRuleDerivativeCanonicalHessian K hK
1904 hFlat
1905 (productRuleDerivativeCanonicalHessian_of_eventuallyZero_and_edgeStencil
1906 K hK hFlat D hZero hEdge hStencil)
1907
1908theorem actionDerivativeTangencyToQuadratic_of_weightedStationary_and_edgeStencil
1909 (K : Triangulation3D) (hK : IncidenceConsistent K)
1910 (hFlat : FlatConfiguration K hK)
1911 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1912 (hStat : WeightedDeficitDerivativeStationaryTarget K hK hFlat)
1913 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1914 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1915 ActionDerivativeTangencyToQuadraticTarget K hK :=
1916 actionDerivativeTangencyToQuadratic_of_flat_productRuleDerivativeCanonicalHessian K hK
1917 hFlat
1918 (productRuleDerivativeCanonicalHessian_of_weightedStationary_and_edgeStencil
1919 K hK hFlat D hStat hEdge hStencil)
1920
1921theorem nonlinearDirectionalHessian_of_eventuallyZero_and_edgeStencil
1922 (K : Triangulation3D) (hK : IncidenceConsistent K)
1923 (hFlat : FlatConfiguration K hK)
1924 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1925 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
1926 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1927 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1928 NonlinearReggeDirectionalHessianTheorem K hK :=
1929 nonlinearDirectionalHessian_of_actionDerivativeTangencyToQuadratic K hK
1930 (actionDerivativeTangencyToQuadratic_of_eventuallyZero_and_edgeStencil
1931 K hK hFlat D hZero hEdge hStencil)
1932
1933theorem nonlinearDirectionalHessian_of_weightedStationary_and_edgeStencil
1934 (K : Triangulation3D) (hK : IncidenceConsistent K)
1935 (hFlat : FlatConfiguration K hK)
1936 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
1937 (hStat : WeightedDeficitDerivativeStationaryTarget K hK hFlat)
1938 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
1939 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
1940 NonlinearReggeDirectionalHessianTheorem K hK :=
1941 nonlinearDirectionalHessian_of_actionDerivativeTangencyToQuadratic K hK
1942 (actionDerivativeTangencyToQuadratic_of_weightedStationary_and_edgeStencil
1943 K hK hFlat D hStat hEdge hStencil)
1944
1945/-- The full nonlinear Hessian proof is reduced to proving zero second
1946variation for the canonical remainder line. The remaining expansion is the
1947Cayley-Menger/arccos chain-rule calculation. -/
1948def NonlinearReggeHessianReducedToRemainder
1949 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1950 ∀ ξ : VertexPotential K,
1951 HasSecondDerivAt (canonicalRemainderAlongLine K hK ξ) 0 0
1952
1953/-- The remaining calculus glue between the explicit action split and the
1954remainder target. This is not the geometric chain-rule calculation itself; it
1955is the exact derivative identity needed because `HasSecondDerivAt` is phrased
1956through `deriv`. Closing it requires first-derivative existence for the
1957action, quadratic line, and subtraction-defined remainder near zero, supplied
1958by the smoothness chain. -/
1959def CanonicalRemainderDerivativeIdentityTarget
1960 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1961 ∀ ξ : VertexPotential K,
1962 (fun t : ℝ => deriv (canonicalRemainderAlongLine K hK ξ) t) =
1963 fun t : ℝ =>
1964 deriv (actionAlongLine K hK ξ) t -
1965 deriv (canonicalQuadraticAlongLine K hK ξ) t
1966
1967/-- Concrete differentiability condition sufficient for the derivative identity.
1968This is the target the smoothness chain should supply for the action line; the
1969quadratic line is elementary. -/
1970def CanonicalRemainderLineDifferentiabilityTarget
1971 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1972 ∀ (ξ : VertexPotential K) (t : ℝ),
1973 DifferentiableAt ℝ (actionAlongLine K hK ξ) t ∧
1974 DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t
1975
1976def ActionLineDifferentiabilityTarget
1977 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1978 ∀ (ξ : VertexPotential K) (t : ℝ),
1979 DifferentiableAt ℝ (actionAlongLine K hK ξ) t
1980
1981def ActionLineDifferentiabilityNearZeroTarget
1982 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
1983 ∀ ξ : VertexPotential K,
1984 ∀ᶠ t : ℝ in nhds (0 : ℝ),
1985 DifferentiableAt ℝ (actionAlongLine K hK ξ) t
1986
1987theorem linePotential_contDiffAt_zero
1988 (K : Triangulation3D) (ξ : VertexPotential K) :
1989 ContDiffAt ℝ (⊤ : ℕ∞) (fun t : ℝ => linePotential K ξ t) (0 : ℝ) := by
1990 rw [contDiffAt_pi]
1991 intro i
1992 unfold linePotential
1993 fun_prop
1994
1995theorem actionAlongLine_contDiffAt_zero_of_flatConfiguration
1996 (K : Triangulation3D) (hK : IncidenceConsistent K)
1997 (hFlat : FlatConfiguration K hK) (ξ : VertexPotential K) :
1998 ContDiffAt ℝ (⊤ : ℕ∞) (actionAlongLine K hK ξ) (0 : ℝ) := by
1999 have hline := linePotential_contDiffAt_zero K ξ
2000 have hActionAt : ContDiffAt ℝ (⊤ : ℕ∞)
2001 (reggeAction K hK) (linePotential K ξ 0) := by
2002 simpa [linePotential_zero K ξ] using hFlat.action_contDiff_at_zero
2003 unfold actionAlongLine
2004 have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hActionAt hline
2005 simpa [Function.comp_def] using hcomp
2006
2007theorem actionLineDifferentiabilityNearZero_of_flatConfiguration
2008 (K : Triangulation3D) (hK : IncidenceConsistent K)
2009 (hFlat : FlatConfiguration K hK) :
2010 ActionLineDifferentiabilityNearZeroTarget K hK := by
2011 intro ξ
2012 exact differentiableAt_eventually_of_contDiffAt_top
2013 (actionAlongLine K hK ξ) 0
2014 (actionAlongLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ)
2015
2016def CanonicalRemainderLineDifferentiabilityNearZeroTarget
2017 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
2018 ∀ ξ : VertexPotential K,
2019 ∀ᶠ t : ℝ in nhds (0 : ℝ),
2020 DifferentiableAt ℝ (actionAlongLine K hK ξ) t ∧
2021 DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t
2022
2023def CanonicalRemainderDerivativeIdentityNearZeroTarget
2024 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
2025 ∀ ξ : VertexPotential K,
2026 (fun t : ℝ => deriv (canonicalRemainderAlongLine K hK ξ) t) =ᶠ[nhds (0 : ℝ)]
2027 ((fun t : ℝ => deriv (actionAlongLine K hK ξ) t) -
2028 fun t : ℝ => deriv (canonicalQuadraticAlongLine K hK ξ) t)
2029
2030theorem canonicalRemainderLineDifferentiability_of_actionLineDifferentiability
2031 (K : Triangulation3D) (hK : IncidenceConsistent K)
2032 (hAction : ActionLineDifferentiabilityTarget K hK) :
2033 CanonicalRemainderLineDifferentiabilityTarget K hK := by
2034 intro ξ t
2035 exact ⟨hAction ξ t, canonicalQuadraticAlongLine_differentiableAt K hK ξ t⟩
2036
2037theorem canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero
2038 (K : Triangulation3D) (hK : IncidenceConsistent K)
2039 (hAction : ActionLineDifferentiabilityNearZeroTarget K hK) :
2040 CanonicalRemainderLineDifferentiabilityNearZeroTarget K hK := by
2041 intro ξ
2042 filter_upwards [hAction ξ] with t ht
2043 exact ⟨ht, canonicalQuadraticAlongLine_differentiableAt K hK ξ t⟩
2044
2045theorem canonicalRemainderDerivativeIdentity_of_lineDifferentiability
2046 (K : Triangulation3D) (hK : IncidenceConsistent K)
2047 (hDiff : CanonicalRemainderLineDifferentiabilityTarget K hK) :
2048 CanonicalRemainderDerivativeIdentityTarget K hK := by
2049 intro ξ
2050 funext t
2051 rw [canonicalRemainderAlongLine_eq_action_sub_quadratic K hK ξ]
2052 have hAction : DifferentiableAt ℝ (actionAlongLine K hK ξ) t := (hDiff ξ t).1
2053 have hQuad : DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t := (hDiff ξ t).2
2054 have hActionSubConst :
2055 DifferentiableAt ℝ
2056 (fun s : ℝ => actionAlongLine K hK ξ s -
2057 reggeAction K hK (zeroPotential K)) t :=
2058 hAction.sub (differentiableAt_const
2059 (c := reggeAction K hK (zeroPotential K)))
2060 have hSub := deriv_sub hActionSubConst hQuad
2061 calc
2062 deriv
2063 (fun s : ℝ =>
2064 actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K) -
2065 canonicalQuadraticAlongLine K hK ξ s) t
2066 = deriv
2067 (fun s : ℝ =>
2068 actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K)) t -
2069 deriv (canonicalQuadraticAlongLine K hK ξ) t := by
2070 simpa [sub_eq_add_neg] using hSub
2071 _ = deriv (actionAlongLine K hK ξ) t -
2072 deriv (canonicalQuadraticAlongLine K hK ξ) t := by
2073 rw [deriv_sub_const]
2074
2075theorem canonicalRemainderDerivativeIdentityNearZero_of_lineDifferentiabilityNearZero
2076 (K : Triangulation3D) (hK : IncidenceConsistent K)
2077 (hDiff : CanonicalRemainderLineDifferentiabilityNearZeroTarget K hK) :
2078 CanonicalRemainderDerivativeIdentityNearZeroTarget K hK := by
2079 intro ξ
2080 filter_upwards [hDiff ξ] with t ht
2081 rw [canonicalRemainderAlongLine_eq_action_sub_quadratic K hK ξ]
2082 have hAction : DifferentiableAt ℝ (actionAlongLine K hK ξ) t := ht.1
2083 have hQuad : DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t := ht.2
2084 have hActionSubConst :
2085 DifferentiableAt ℝ
2086 (fun s : ℝ => actionAlongLine K hK ξ s -
2087 reggeAction K hK (zeroPotential K)) t :=
2088 hAction.sub (differentiableAt_const
2089 (c := reggeAction K hK (zeroPotential K)))
2090 have hSub := deriv_sub hActionSubConst hQuad
2091 calc
2092 deriv
2093 (fun s : ℝ =>
2094 actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K) -
2095 canonicalQuadraticAlongLine K hK ξ s) t
2096 = deriv
2097 (fun s : ℝ =>
2098 actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K)) t -
2099 deriv (canonicalQuadraticAlongLine K hK ξ) t := by
2100 simpa [sub_eq_add_neg] using hSub
2101 _ = deriv (actionAlongLine K hK ξ) t -
2102 deriv (canonicalQuadraticAlongLine K hK ξ) t := by
2103 rw [deriv_sub_const]
2104
2105theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_derivIdentity
2106 (K : Triangulation3D) (hK : IncidenceConsistent K)
2107 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
2108 (hDeriv : CanonicalRemainderDerivativeIdentityTarget K hK) :
2109 CanonicalRemainderSecondVariationZero K hK := by
2110 intro ξ
2111 unfold HasSecondDerivAt
2112 change HasDerivAt
2113 (fun t : ℝ => deriv (canonicalRemainderAlongLine K hK ξ) t) 0 0
2114 rw [hDeriv ξ]
2115 have hAction : HasDerivAt
2116 (fun t : ℝ => deriv (actionAlongLine K hK ξ) t)
2117 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := hHessian ξ
2118 have hQuadRaw := canonicalQuadraticAlongLine_hasSecondDerivAt_zero K hK ξ
2119 have hQuad : HasDerivAt
2120 (fun t : ℝ => deriv (canonicalQuadraticAlongLine K hK ξ) t)
2121 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := hQuadRaw
2122 have hSub := hAction.sub hQuad
2123 simpa using hSub
2124
2125theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_derivIdentityNearZero
2126 (K : Triangulation3D) (hK : IncidenceConsistent K)
2127 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
2128 (hDeriv : CanonicalRemainderDerivativeIdentityNearZeroTarget K hK) :
2129 CanonicalRemainderSecondVariationZero K hK := by
2130 intro ξ
2131 unfold HasSecondDerivAt
2132 change HasDerivAt
2133 (fun t : ℝ => deriv (canonicalRemainderAlongLine K hK ξ) t) 0 0
2134 have hAction : HasDerivAt
2135 (fun t : ℝ => deriv (actionAlongLine K hK ξ) t)
2136 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := hHessian ξ
2137 have hQuadRaw := canonicalQuadraticAlongLine_hasSecondDerivAt_zero K hK ξ
2138 have hQuad : HasDerivAt
2139 (fun t : ℝ => deriv (canonicalQuadraticAlongLine K hK ξ) t)
2140 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 := hQuadRaw
2141 have hSub := hAction.sub hQuad
2142 simpa using hSub.congr_of_eventuallyEq (hDeriv ξ)
2143
2144theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_lineDiff
2145 (K : Triangulation3D) (hK : IncidenceConsistent K)
2146 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
2147 (hDiff : CanonicalRemainderLineDifferentiabilityTarget K hK) :
2148 CanonicalRemainderSecondVariationZero K hK :=
2149 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_derivIdentity
2150 K hK hHessian
2151 (canonicalRemainderDerivativeIdentity_of_lineDifferentiability K hK hDiff)
2152
2153theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_actionLineDiff
2154 (K : Triangulation3D) (hK : IncidenceConsistent K)
2155 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
2156 (hAction : ActionLineDifferentiabilityTarget K hK) :
2157 CanonicalRemainderSecondVariationZero K hK :=
2158 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_lineDiff
2159 K hK hHessian
2160 (canonicalRemainderLineDifferentiability_of_actionLineDifferentiability K hK hAction)
2161
2162theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_actionLineDiffNearZero
2163 (K : Triangulation3D) (hK : IncidenceConsistent K)
2164 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
2165 (hAction : ActionLineDifferentiabilityNearZeroTarget K hK) :
2166 CanonicalRemainderSecondVariationZero K hK :=
2167 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_derivIdentityNearZero
2168 K hK hHessian
2169 (canonicalRemainderDerivativeIdentityNearZero_of_lineDifferentiabilityNearZero K hK
2170 (canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero
2171 K hK hAction))
2172
2173theorem canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration
2174 (K : Triangulation3D) (hK : IncidenceConsistent K)
2175 (hFlat : FlatConfiguration K hK)
2176 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK) :
2177 CanonicalRemainderSecondVariationZero K hK :=
2178 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_actionLineDiffNearZero
2179 K hK hHessian
2180 (actionLineDifferentiabilityNearZero_of_flatConfiguration K hK hFlat)
2181
2182theorem canonicalRemainderSecondVariationZero_of_actionDerivativeLinearizationNearZero_and_flat
2183 (K : Triangulation3D) (hK : IncidenceConsistent K)
2184 (hFlat : FlatConfiguration K hK)
2185 (hLin : ActionDerivativeLinearizationNearZeroTarget K hK) :
2186 CanonicalRemainderSecondVariationZero K hK :=
2187 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration
2188 K hK hFlat
2189 (nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero K hK hLin)
2190
2191theorem canonicalRemainderSecondVariationZero_of_actionDerivativeTangency_and_flat
2192 (K : Triangulation3D) (hK : IncidenceConsistent K)
2193 (hFlat : FlatConfiguration K hK)
2194 (hTan : ActionDerivativeFirstOrderTangencyTarget K hK) :
2195 CanonicalRemainderSecondVariationZero K hK :=
2196 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration
2197 K hK hFlat
2198 (nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency K hK hTan)
2199
2200def reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian
2201 (K : Triangulation3D) (hK : IncidenceConsistent K)
2202 (hFlat : FlatConfiguration K hK)
2203 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK) :
2204 ReggeActionRemainderSecondVariationInput K hK where
2205 remainder_secondVariation_zero :=
2206 canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration
2207 K hK hFlat hHessian
2208
2209def reggeActionSecondVariationInput_of_flat_nonlinearHessian
2210 (K : Triangulation3D) (hK : IncidenceConsistent K)
2211 (hFlat : FlatConfiguration K hK)
2212 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK) :
2213 ReggeActionSecondVariationInput K hK hFlat :=
2214 reggeActionSecondVariationInput_of_directionalSecondVariation
2215 K hK hFlat hHessian
2216
2217def reggeActionRemainderSecondVariationInput_of_eventuallyZero_and_edgeStencil
2218 (K : Triangulation3D) (hK : IncidenceConsistent K)
2219 (hFlat : FlatConfiguration K hK)
2220 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
2221 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
2222 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
2223 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
2224 ReggeActionRemainderSecondVariationInput K hK :=
2225 reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
2226 (nonlinearDirectionalHessian_of_eventuallyZero_and_edgeStencil
2227 K hK hFlat D hZero hEdge hStencil)
2228
2229def reggeActionSecondVariationInput_of_eventuallyZero_and_edgeStencil
2230 (K : Triangulation3D) (hK : IncidenceConsistent K)
2231 (hFlat : FlatConfiguration K hK)
2232 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
2233 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
2234 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
2235 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK) :
2236 ReggeActionSecondVariationInput K hK hFlat :=
2237 reggeActionSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
2238 (nonlinearDirectionalHessian_of_eventuallyZero_and_edgeStencil
2239 K hK hFlat D hZero hEdge hStencil)
2240
2241def reggeActionRemainderSecondVariationInput_of_flat_actionDerivativeLinearization
2242 (K : Triangulation3D) (hK : IncidenceConsistent K)
2243 (hFlat : FlatConfiguration K hK)
2244 (hLin : ActionDerivativeLinearizationNearZeroTarget K hK) :
2245 ReggeActionRemainderSecondVariationInput K hK where
2246 remainder_secondVariation_zero :=
2247 canonicalRemainderSecondVariationZero_of_actionDerivativeLinearizationNearZero_and_flat
2248 K hK hFlat hLin
2249
2250def reggeActionSecondVariationInput_of_flat_actionDerivativeLinearization
2251 (K : Triangulation3D) (hK : IncidenceConsistent K)
2252 (hFlat : FlatConfiguration K hK)
2253 (hLin : ActionDerivativeLinearizationNearZeroTarget K hK) :
2254 ReggeActionSecondVariationInput K hK hFlat :=
2255 reggeActionSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
2256 (nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero K hK hLin)
2257
2258def reggeActionRemainderSecondVariationInput_of_flat_actionDerivativeTangency
2259 (K : Triangulation3D) (hK : IncidenceConsistent K)
2260 (hFlat : FlatConfiguration K hK)
2261 (hTan : ActionDerivativeFirstOrderTangencyTarget K hK) :
2262 ReggeActionRemainderSecondVariationInput K hK where
2263 remainder_secondVariation_zero :=
2264 canonicalRemainderSecondVariationZero_of_actionDerivativeTangency_and_flat
2265 K hK hFlat hTan
2266
2267def reggeActionSecondVariationInput_of_flat_actionDerivativeTangency
2268 (K : Triangulation3D) (hK : IncidenceConsistent K)
2269 (hFlat : FlatConfiguration K hK)
2270 (hTan : ActionDerivativeFirstOrderTangencyTarget K hK) :
2271 ReggeActionSecondVariationInput K hK hFlat :=
2272 reggeActionSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
2273 (nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency K hK hTan)
2274
2275def reggeActionRemainderSecondVariationInput_of_flat_actionDerivativeTangencyToQuadratic
2276 (K : Triangulation3D) (hK : IncidenceConsistent K)
2277 (hFlat : FlatConfiguration K hK)
2278 (hTan : ActionDerivativeTangencyToQuadraticTarget K hK) :
2279 ReggeActionRemainderSecondVariationInput K hK :=
2280 reggeActionRemainderSecondVariationInput_of_flat_actionDerivativeTangency
2281 K hK hFlat
2282 (actionDerivativeFirstOrderTangency_of_quadraticTangency K hK hTan)
2283
2284def reggeActionSecondVariationInput_of_flat_actionDerivativeTangencyToQuadratic
2285 (K : Triangulation3D) (hK : IncidenceConsistent K)
2286 (hFlat : FlatConfiguration K hK)
2287 (hTan : ActionDerivativeTangencyToQuadraticTarget K hK) :
2288 ReggeActionSecondVariationInput K hK hFlat :=
2289 reggeActionSecondVariationInput_of_flat_actionDerivativeTangency
2290 K hK hFlat
2291 (actionDerivativeFirstOrderTangency_of_quadraticTangency K hK hTan)
2292
2293theorem remainder_reduction_eq_canonicalRemainderSecondVariation
2294 (K : Triangulation3D) (hK : IncidenceConsistent K) :
2295 NonlinearReggeHessianReducedToRemainder K hK ↔
2296 CanonicalRemainderSecondVariationZero K hK := by
2297 rfl
2298
2299theorem canonicalRemainderSecondVariationZero_of_identically_zero
2300 (K : Triangulation3D) (hK : IncidenceConsistent K)
2301 (hZero :
2302 ∀ ξ : VertexPotential K,
2303 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
2304 CanonicalRemainderSecondVariationZero K hK := by
2305 intro ξ
2306 unfold HasSecondDerivAt
2307 have hfun :
2308 (fun t : ℝ =>
2309 reggeActionRemainder K hK (canonicalReggeHessian K hK)
2310 (linePotential K ξ t)) = fun _t : ℝ => (0 : ℝ) := by
2311 funext t
2312 exact hZero (linePotential K ξ t)
2313 rw [hfun]
2314 simpa using (hasDerivAt_const (x := (0 : ℝ)) (c := (0 : ℝ)))
2315
2316theorem nonlinearDirectionalHessian_of_remainder_identically_zero
2317 (K : Triangulation3D) (hK : IncidenceConsistent K)
2318 (hZero :
2319 ∀ ξ : VertexPotential K,
2320 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
2321 NonlinearReggeDirectionalHessianTheorem K hK := by
2322 intro ξ
2323 have hsplit := actionAlongLine_canonical_split K hK ξ
2324 have haction :
2325 actionAlongLine K hK ξ =
2326 fun t : ℝ =>
2327 reggeAction K hK (zeroPotential K) +
2328 canonicalQuadraticAlongLine K hK ξ t := by
2329 funext t
2330 rw [congrFun hsplit t]
2331 simp [canonicalRemainderAlongLine, hZero]
2332 have hquad := canonicalQuadraticAlongLine_hasSecondDerivAt_zero K hK ξ
2333 have hconst :=
2334 hasSecondDerivAt_const_add
2335 (canonicalQuadraticAlongLine K hK ξ)
2336 (reggeAction K hK (zeroPotential K))
2337 (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0 hquad
2338 simpa [haction] using hconst
2339
2340theorem canonicalHessianSecondVariation_of_nonlinearDirectionalHessian
2341 (K : Triangulation3D) (hK : IncidenceConsistent K)
2342 (h : NonlinearReggeDirectionalHessianTheorem K hK) :
2343 CanonicalHessianSecondVariationAtZero K hK :=
2344 h
2345
2346def reggeActionSecondVariationInput_of_nonlinearDirectionalHessian
2347 (K : Triangulation3D) (hK : IncidenceConsistent K)
2348 (hFlat : FlatConfiguration K hK)
2349 (h : NonlinearReggeDirectionalHessianTheorem K hK) :
2350 ReggeActionSecondVariationInput K hK hFlat :=
2351 reggeActionSecondVariationInput_of_directionalSecondVariation K hK hFlat
2352 (canonicalHessianSecondVariation_of_nonlinearDirectionalHessian K hK h)
2353
2354/-- A convenient equivalent formulation in terms of the canonical nonlinear
2355remainder: if the canonical remainder has zero second variation in every
2356direction, then the nonlinear Hessian is canonical. -/
2357def CanonicalRemainderZeroSecondVariationTheorem
2358 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
2359 CanonicalRemainderSecondVariationZero K hK
2360
2361def reggeActionRemainderSecondVariationInput_of_theorem
2362 (K : Triangulation3D) (hK : IncidenceConsistent K)
2363 (h : CanonicalRemainderZeroSecondVariationTheorem K hK) :
2364 ReggeActionRemainderSecondVariationInput K hK where
2365 remainder_secondVariation_zero := h
2366
2367end
2368
2369end ReggeActionNonlinearHessianProof
2370end Geometry
2371end IndisputableMonolith
2372