IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound
IndisputableMonolith/Geometry/ReggeActionCubicTaylorBound.lean · 1186 lines · 55 declarations
show as:
view math explainer →
1import IndisputableMonolith.Geometry.ReggeActionNonlinearHessianProof
2
3/-!
4# Cubic Taylor Bound for the Nonlinear Regge Remainder
5
6This module isolates the final analytic Taylor theorem needed after the
7nonlinear Hessian has been identified. The heavy analytic content is a local
8third-order bound in the finite-dimensional vertex-potential space.
9-/
10
11namespace IndisputableMonolith
12namespace Geometry
13namespace ReggeActionCubicTaylorBound
14
15open ReggeTriangulation3D
16open ReggeHessian3D
17open Triangulation3DConsistency
18open ReggeActionConcrete
19open ReggeActionSmoothness
20open ReggeActionSecondVariation
21open ReggeActionNonlinearHessianProof
22
23noncomputable section
24
25/-- Exact Taylor theorem needed for the nonlinear Regge remainder. This is
26the finite-dimensional third-order Taylor estimate specialized to the canonical
27Regge remainder. -/
28def NonlinearReggeCubicTaylorTheorem
29 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
30 LocalCubicRemainderBound K hK
31
32def reggeActionCubicRemainderInput_of_taylorTheorem
33 (K : Triangulation3D) (hK : IncidenceConsistent K)
34 (hFlat : FlatConfiguration K hK)
35 (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
36 ReggeActionCubicRemainderInput K hK hFlat :=
37 reggeActionCubicRemainderInput_of_bound K hK hFlat hTaylor
38
39/-- The Taylor theorem is exactly the local cubic remainder bound. This
40identity lemma makes the audit explicit: no hidden analytic assumption is
41buried in the constructor. -/
42theorem nonlinearReggeCubicTaylorTheorem_iff_localBound
43 (K : Triangulation3D) (hK : IncidenceConsistent K) :
44 NonlinearReggeCubicTaylorTheorem K hK ↔ LocalCubicRemainderBound K hK :=
45 Iff.rfl
46
47/-- If the canonical nonlinear remainder vanishes identically, the cubic Taylor
48theorem follows with zero constant. The real nonlinear theorem will replace
49this strong special case by the finite-dimensional third-order estimate. -/
50theorem nonlinearReggeCubicTaylorTheorem_of_identically_zero
51 (K : Triangulation3D) (hK : IncidenceConsistent K)
52 (hZero :
53 ∀ ξ : VertexPotential K,
54 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
55 NonlinearReggeCubicTaylorTheorem K hK := by
56 refine ⟨1, 0, by norm_num, le_rfl, ?_⟩
57 intro ξ _hξ
58 rw [hZero ξ]
59 simp
60
61theorem canonicalRemainder_contDiffAt_zero_of_flatConfiguration
62 (K : Triangulation3D) (hK : IncidenceConsistent K)
63 (hFlat : FlatConfiguration K hK) :
64 ContDiffAt ℝ (⊤ : ℕ∞)
65 (fun ξ : VertexPotential K =>
66 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ)
67 (zeroPotential K) := by
68 unfold reggeActionRemainder
69 have hAction := hFlat.action_contDiff_at_zero
70 have hConst : ContDiffAt ℝ (⊤ : ℕ∞)
71 (fun _ξ : VertexPotential K => reggeAction K hK (zeroPotential K))
72 (zeroPotential K) := contDiffAt_const
73 have hQuad : ContDiffAt ℝ (⊤ : ℕ∞)
74 (fun ξ : VertexPotential K =>
75 (1 / 2) * hessianQuadratic (canonicalReggeHessian K hK) ξ)
76 (zeroPotential K) := by
77 unfold hessianQuadratic
78 fun_prop
79 exact (hAction.sub hConst).sub hQuad
80
81/-- The exact remaining finite-dimensional Taylor theorem.
82
83The canonical remainder is already smooth at the flat point and its value is
84zero. To derive the cubic estimate from standard Taylor theory, it remains to
85connect the zero first-variation and zero second-variation inputs for the
86canonical remainder to a local `O(||ξ||^3)` bound. This definition isolates
87that analytic theorem without adding an axiom. -/
88def CanonicalRemainderCubicTaylorFromJetInputsTarget
89 (K : Triangulation3D) (hK : IncidenceConsistent K)
90 (_hFlat : FlatConfiguration K hK) : Prop :=
91 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
92 (canonicalReggeHessian K hK) →
93 ReggeActionRemainderSecondVariationInput K hK →
94 NonlinearReggeCubicTaylorTheorem K hK
95
96theorem nonlinearReggeCubicTaylorTheorem_of_remainderJetInputs
97 (K : Triangulation3D) (hK : IncidenceConsistent K)
98 (hFlat : FlatConfiguration K hK)
99 (hTaylorFromJets : CanonicalRemainderCubicTaylorFromJetInputsTarget K hK hFlat)
100 (hFirst :
101 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
102 (canonicalReggeHessian K hK))
103 (hSecond : ReggeActionRemainderSecondVariationInput K hK) :
104 NonlinearReggeCubicTaylorTheorem K hK :=
105 hTaylorFromJets hFirst hSecond
106
107theorem linePotential_one
108 (K : Triangulation3D) (ξ : VertexPotential K) :
109 linePotential K ξ 1 = ξ := by
110 funext i
111 simp [linePotential]
112
113theorem linePotential_eq_smul
114 (K : Triangulation3D) (ξ : VertexPotential K) (t : ℝ) :
115 linePotential K ξ t = t • ξ := by
116 funext i
117 simp [linePotential]
118
119theorem norm_linePotential_le_of_mem_Icc_zero_one
120 (K : Triangulation3D) (ξ : VertexPotential K) {t : ℝ}
121 (ht : t ∈ Set.Icc (0 : ℝ) 1) :
122 ‖linePotential K ξ t‖ ≤ ‖ξ‖ := by
123 rw [linePotential_eq_smul K ξ t, norm_smul, Real.norm_eq_abs]
124 have habs : |t| ≤ 1 := by
125 rw [abs_of_nonneg ht.1]
126 exact ht.2
127 calc
128 |t| * ‖ξ‖ ≤ 1 * ‖ξ‖ :=
129 mul_le_mul_of_nonneg_right habs (norm_nonneg ξ)
130 _ = ‖ξ‖ := one_mul _
131
132/-- One-dimensional line form of the remaining cubic Taylor estimate.
133
134For every conformal direction `ξ`, restrict the canonical remainder to the line
135`t ↦ tξ`. A standard one-variable Taylor theorem with zero value, first
136variation, and second variation at `t = 0` should prove this estimate from a
137uniform bound on third derivatives along the segment. -/
138def CanonicalRemainderLineCubicEstimateTarget
139 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
140 ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
141 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
142 ‖reggeActionRemainder K hK (canonicalReggeHessian K hK)
143 (linePotential K ξ 1)‖ ≤
144 C * ‖ξ‖ ^ (3 : ℕ)
145
146theorem nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate
147 (K : Triangulation3D) (hK : IncidenceConsistent K)
148 (hLine : CanonicalRemainderLineCubicEstimateTarget K hK) :
149 NonlinearReggeCubicTaylorTheorem K hK := by
150 rcases hLine with ⟨r, C, hr, hC, hineq⟩
151 refine ⟨r, C, hr, hC, ?_⟩
152 intro ξ hξ
153 simpa [linePotential_one K ξ] using hineq ξ hξ
154
155private theorem abs_value_le_cubic_of_taylor_data
156 (f : ℝ → ℝ) (M a : ℝ)
157 (hf : ContDiffOn ℝ (3 : ℕ) f (Set.Icc (0 : ℝ) 1))
158 (hTaylorZero : taylorWithinEval f 2 (Set.Icc (0 : ℝ) 1) 0 1 = 0)
159 (hbound : ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv 3 f t| ≤ M * a) :
160 |f 1| ≤ (M / 6) * a := by
161 have hrem :=
162 taylor_mean_remainder_lagrange_iteratedDeriv
163 (f := f) (x₀ := (0 : ℝ)) (x := (1 : ℝ)) (n := 2)
164 (by norm_num) (by simpa using hf)
165 rcases hrem with ⟨x', hx', hEq⟩
166 rw [hTaylorZero] at hEq
167 have hxIcc : x' ∈ Set.Icc (0 : ℝ) 1 :=
168 ⟨le_of_lt hx'.1, le_of_lt hx'.2⟩
169 have hb := hbound x' hxIcc
170 rw [sub_zero] at hEq
171 rw [hEq]
172 norm_num
173 rw [abs_div]
174 norm_num
175 have hdiv : |iteratedDeriv 3 f x'| / (6 : ℝ) ≤ (M * a) / 6 :=
176 div_le_div_of_nonneg_right hb (by norm_num : (0 : ℝ) ≤ 6)
177 have hrewrite : (M * a) / 6 = (M / 6) * a := by ring
178 rwa [hrewrite] at hdiv
179
180/-- Mathlib-shaped one-variable Taylor data along every conformal line.
181
182This is the precise analytic bridge left after all geometric reductions:
183for each direction `ξ`, the line-restricted canonical remainder is `C^3` on the
184unit segment, its quadratic Taylor polynomial at zero vanishes, and its third
185derivative is bounded by `M * ||ξ||^3` on the segment. -/
186def CanonicalRemainderLineTaylorDataTarget
187 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
188 ∃ (r M : ℝ), 0 < r ∧ 0 ≤ M ∧
189 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
190 ContDiffOn ℝ (3 : ℕ)
191 (fun t : ℝ =>
192 reggeActionRemainder K hK (canonicalReggeHessian K hK)
193 (linePotential K ξ t))
194 (Set.Icc (0 : ℝ) 1) ∧
195 taylorWithinEval
196 (fun t : ℝ =>
197 reggeActionRemainder K hK (canonicalReggeHessian K hK)
198 (linePotential K ξ t))
199 2 (Set.Icc (0 : ℝ) 1) 0 1 = 0 ∧
200 ∀ t ∈ Set.Icc (0 : ℝ) 1,
201 |iteratedDeriv 3
202 (fun s : ℝ =>
203 reggeActionRemainder K hK (canonicalReggeHessian K hK)
204 (linePotential K ξ s)) t| ≤ M * ‖ξ‖ ^ (3 : ℕ)
205
206def CanonicalRemainderLineContDiffTarget
207 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
208 ∃ r : ℝ, 0 < r ∧
209 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
210 ContDiffOn ℝ (3 : ℕ)
211 (fun t : ℝ =>
212 reggeActionRemainder K hK (canonicalReggeHessian K hK)
213 (linePotential K ξ t))
214 (Set.Icc (0 : ℝ) 1)
215
216theorem canonicalRemainderLineContDiff_of_flatConfiguration
217 (K : Triangulation3D) (hK : IncidenceConsistent K)
218 (hFlat : FlatConfiguration K hK) :
219 CanonicalRemainderLineContDiffTarget K hK := by
220 let R : VertexPotential K → ℝ :=
221 fun ξ => reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ
222 have hR : ContDiffAt ℝ (⊤ : ℕ∞) R (zeroPotential K) := by
223 simpa [R] using canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
224 have hle : ((3 : ℕ∞) : WithTop ℕ∞) ≤ ((⊤ : ℕ∞) : WithTop ℕ∞) := by
225 exact WithTop.coe_le_coe.2 le_top
226 rcases hR.contDiffOn (m := (3 : ℕ∞)) hle (by intro h; simp at h) with
227 ⟨u, hu, hRu⟩
228 rcases Metric.mem_nhds_iff.mp hu with ⟨eps, heps, hball⟩
229 refine ⟨eps, heps, ?_⟩
230 intro ξ hξ
231 have hline : ContDiffOn ℝ (3 : ℕ∞)
232 (fun t : ℝ => linePotential K ξ t) (Set.Icc (0 : ℝ) 1) := by
233 rw [contDiffOn_pi]
234 intro i
235 unfold linePotential
236 fun_prop
237 have hmaps : Set.MapsTo (fun t : ℝ => linePotential K ξ t)
238 (Set.Icc (0 : ℝ) 1) u := by
239 intro t ht
240 apply hball
241 rw [Metric.mem_ball, dist_eq_norm]
242 have hsub : linePotential K ξ t - zeroPotential K = linePotential K ξ t := by
243 funext i
244 simp [zeroPotential]
245 rw [hsub]
246 exact lt_of_le_of_lt (norm_linePotential_le_of_mem_Icc_zero_one K ξ ht) hξ
247 have hcomp := hRu.comp hline hmaps
248 simpa [R, Function.comp_def] using hcomp
249
250def CanonicalRemainderLineQuadraticTaylorZeroTarget
251 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
252 ∃ r : ℝ, 0 < r ∧
253 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
254 taylorWithinEval
255 (fun t : ℝ =>
256 reggeActionRemainder K hK (canonicalReggeHessian K hK)
257 (linePotential K ξ t))
258 2 (Set.Icc (0 : ℝ) 1) 0 1 = 0
259
260def CanonicalRemainderLineThirdDerivBoundTarget
261 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
262 ∃ (r M : ℝ), 0 < r ∧ 0 ≤ M ∧
263 ∀ ξ : VertexPotential K, ‖ξ‖ < r →
264 ∀ t ∈ Set.Icc (0 : ℝ) 1,
265 |iteratedDeriv 3
266 (fun s : ℝ =>
267 reggeActionRemainder K hK (canonicalReggeHessian K hK)
268 (linePotential K ξ s)) t| ≤ M * ‖ξ‖ ^ (3 : ℕ)
269
270private theorem min_pos3 {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
271 0 < min (min a b) c :=
272 lt_min (lt_min ha hb) hc
273
274theorem lineTaylorData_of_splitTargets
275 (K : Triangulation3D) (hK : IncidenceConsistent K)
276 (hCont : CanonicalRemainderLineContDiffTarget K hK)
277 (hTaylorZero : CanonicalRemainderLineQuadraticTaylorZeroTarget K hK)
278 (hThird : CanonicalRemainderLineThirdDerivBoundTarget K hK) :
279 CanonicalRemainderLineTaylorDataTarget K hK := by
280 rcases hCont with ⟨rC, hrC, hC⟩
281 rcases hTaylorZero with ⟨rT, hrT, hT⟩
282 rcases hThird with ⟨rD, M, hrD, hM, hD⟩
283 refine ⟨min (min rC rT) rD, M, min_pos3 hrC hrT hrD, hM, ?_⟩
284 intro ξ hξ
285 have hξC : ‖ξ‖ < rC := lt_of_lt_of_le hξ (min_le_left (min rC rT) rD |>.trans (min_le_left rC rT))
286 have hξT : ‖ξ‖ < rT := by
287 have hle : min (min rC rT) rD ≤ rT :=
288 le_trans (min_le_left (min rC rT) rD) (min_le_right rC rT)
289 exact lt_of_lt_of_le hξ hle
290 have hξD : ‖ξ‖ < rD := lt_of_lt_of_le hξ (min_le_right (min rC rT) rD)
291 exact ⟨hC ξ hξC, hT ξ hξT, hD ξ hξD⟩
292
293theorem lineCubicEstimate_of_lineTaylorData
294 (K : Triangulation3D) (hK : IncidenceConsistent K)
295 (hData : CanonicalRemainderLineTaylorDataTarget K hK) :
296 CanonicalRemainderLineCubicEstimateTarget K hK := by
297 rcases hData with ⟨r, M, hr, hM, hdata⟩
298 refine ⟨r, M / 6, hr, div_nonneg hM (by norm_num), ?_⟩
299 intro ξ hξ
300 rcases hdata ξ hξ with ⟨hCont, hTaylorZero, hBound⟩
301 have h :=
302 abs_value_le_cubic_of_taylor_data
303 (fun t : ℝ =>
304 reggeActionRemainder K hK (canonicalReggeHessian K hK)
305 (linePotential K ξ t))
306 M (‖ξ‖ ^ (3 : ℕ)) hCont hTaylorZero hBound
307 simpa [Real.norm_eq_abs] using h
308
309theorem nonlinearReggeCubicTaylorTheorem_of_lineTaylorData
310 (K : Triangulation3D) (hK : IncidenceConsistent K)
311 (hData : CanonicalRemainderLineTaylorDataTarget K hK) :
312 NonlinearReggeCubicTaylorTheorem K hK :=
313 nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate K hK
314 (lineCubicEstimate_of_lineTaylorData K hK hData)
315
316/-- Once the nonlinear Hessian is identified and the cubic Taylor theorem is
317proved, the canonical nonlinear remainder is controlled by `O(||xi||^3)`. -/
318def cubicRemainderInput_of_hessian_and_taylor
319 (K : Triangulation3D) (hK : IncidenceConsistent K)
320 (hFlat : FlatConfiguration K hK)
321 (_hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
322 (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
323 ReggeActionCubicRemainderInput K hK hFlat :=
324 reggeActionCubicRemainderInput_of_taylorTheorem K hK hFlat hTaylor
325
326/-- Combined local nonlinear inputs after the Hessian branch and the cubic
327Taylor branch have both been supplied. The fields are theorem-valued outputs,
328not new assumptions. -/
329structure NonlinearReggeLocalHessianTaylorInputs
330 (K : Triangulation3D) (hK : IncidenceConsistent K)
331 (hFlat : FlatConfiguration K hK) where
332 action_secondVariation : ReggeActionSecondVariationInput K hK hFlat
333 remainder_secondVariation : ReggeActionRemainderSecondVariationInput K hK
334 cubic_remainder : ReggeActionCubicRemainderInput K hK hFlat
335
336def nonlinearReggeLocalHessianTaylorInputs_of_hessian_and_taylor
337 (K : Triangulation3D) (hK : IncidenceConsistent K)
338 (hFlat : FlatConfiguration K hK)
339 (hHessian : NonlinearReggeDirectionalHessianTheorem K hK)
340 (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
341 NonlinearReggeLocalHessianTaylorInputs K hK hFlat where
342 action_secondVariation :=
343 reggeActionSecondVariationInput_of_flat_nonlinearHessian K hK hFlat hHessian
344 remainder_secondVariation :=
345 reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian K hK hFlat
346 hHessian
347 cubic_remainder :=
348 cubicRemainderInput_of_hessian_and_taylor K hK hFlat hHessian hTaylor
349
350def nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor
351 (K : Triangulation3D) (hK : IncidenceConsistent K)
352 (hFlat : FlatConfiguration K hK)
353 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
354 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
355 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
356 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK)
357 (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
358 NonlinearReggeLocalHessianTaylorInputs K hK hFlat where
359 action_secondVariation :=
360 reggeActionSecondVariationInput_of_eventuallyZero_and_edgeStencil
361 K hK hFlat D hZero hEdge hStencil
362 remainder_secondVariation :=
363 reggeActionRemainderSecondVariationInput_of_eventuallyZero_and_edgeStencil
364 K hK hFlat D hZero hEdge hStencil
365 cubic_remainder :=
366 reggeActionCubicRemainderInput_of_taylorTheorem K hK hFlat hTaylor
367
368def nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_remainderJetTarget
369 (K : Triangulation3D) (hK : IncidenceConsistent K)
370 (hFlat : FlatConfiguration K hK)
371 (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
372 (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
373 (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
374 (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK)
375 (hTaylorFromJets : CanonicalRemainderCubicTaylorFromJetInputsTarget K hK hFlat)
376 (hFirst :
377 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
378 (canonicalReggeHessian K hK)) :
379 NonlinearReggeLocalHessianTaylorInputs K hK hFlat :=
380 nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor
381 K hK hFlat D hZero hEdge hStencil
382 (hTaylorFromJets hFirst
383 (reggeActionRemainderSecondVariationInput_of_eventuallyZero_and_edgeStencil
384 K hK hFlat D hZero hEdge hStencil))
385
386/-! ## §6. Closure of `CanonicalRemainderLineQuadraticTaylorZeroTarget`
387
388This section discharges the second of the three sub-targets that compose
389`CanonicalRemainderLineTaylorDataTarget`. The first
390(`CanonicalRemainderLineContDiffTarget`) was already closed by
391`canonicalRemainderLineContDiff_of_flatConfiguration` above. The third
392(`CanonicalRemainderLineThirdDerivBoundTarget`) is closed later in this file by
393`canonicalRemainderLineThirdDerivBound_of_flatConfiguration`.
394
395The strategy here is direct: the remainder's quadratic Taylor polynomial at
396zero, restricted to the conformal line, vanishes because:
397* `R(0) = 0` (`reggeActionRemainder_zero`),
398* `R'(0) = 0` along every line (`fderiv R 0 = 0` from
399 `ReggeActionRemainderFirstVariationInput`),
400* `R''(0) = 0` along every line (`HasSecondDerivAt R_line 0 0` from
401 `ReggeActionRemainderSecondVariationInput`).
402The bridge from `iteratedDerivWithin` to free-space `iteratedDeriv` uses
403`uniqueDiffOn_Icc_zero_one` and `ContDiffAt` (the latter inherited from
404`canonicalRemainder_contDiffAt_zero_of_flatConfiguration` plus C^∞ of the
405linear line map). -/
406
407/-- ContDiffAt of the line-restricted canonical remainder at `t = 0`. -/
408theorem canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration
409 (K : Triangulation3D) (hK : IncidenceConsistent K)
410 (hFlat : FlatConfiguration K hK) (ξ : VertexPotential K) :
411 ContDiffAt ℝ (⊤ : ℕ∞)
412 (fun t : ℝ =>
413 reggeActionRemainder K hK (canonicalReggeHessian K hK)
414 (linePotential K ξ t)) 0 := by
415 have hR : ContDiffAt ℝ (⊤ : ℕ∞)
416 (fun ξ' : VertexPotential K =>
417 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
418 (zeroPotential K) :=
419 canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
420 have hLine : ContDiffAt ℝ (⊤ : ℕ∞)
421 (fun t : ℝ => linePotential K ξ t) 0 := by
422 rw [contDiffAt_pi]
423 intro i
424 show ContDiffAt ℝ (⊤ : ℕ∞) (fun t : ℝ => t * ξ i) 0
425 fun_prop
426 -- Rewrite the target point using `linePotential K ξ 0 = zeroPotential K`.
427 have hLine0 : linePotential K ξ 0 = zeroPotential K := linePotential_zero K ξ
428 have hR' : ContDiffAt ℝ (⊤ : ℕ∞)
429 (fun ξ' : VertexPotential K =>
430 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
431 (linePotential K ξ 0) := by
432 rw [hLine0]; exact hR
433 exact hR'.comp 0 hLine
434
435/-- `R(linePotential ξ 0) = 0`. -/
436theorem canonicalRemainderLine_value_at_zero
437 (K : Triangulation3D) (hK : IncidenceConsistent K)
438 (ξ : VertexPotential K) :
439 reggeActionRemainder K hK (canonicalReggeHessian K hK)
440 (linePotential K ξ 0) = 0 := by
441 rw [linePotential_zero K ξ]
442 exact ReggeActionConcrete.reggeActionRemainder_zero K hK _
443
444/-- The line `t ↦ t • ξ` has derivative `ξ` at every point. -/
445private theorem hasDerivAt_linePotential
446 (K : Triangulation3D) (ξ : VertexPotential K) (t : ℝ) :
447 HasDerivAt (fun s : ℝ => linePotential K ξ s) ξ t := by
448 rw [show (fun s : ℝ => linePotential K ξ s) = (fun s : ℝ => s • ξ) by
449 funext s; rw [linePotential_eq_smul]]
450 -- HasDerivAt (· • ξ) ξ t : derivative of t ↦ t • ξ is ξ.
451 have h := (hasDerivAt_id t).smul_const ξ
452 simpa using h
453
454/-- The line-restricted remainder has derivative 0 at 0, given the remainder's
455free-space gradient vanishes at 0. -/
456theorem canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar
457 (K : Triangulation3D) (hK : IncidenceConsistent K)
458 (hFlat : FlatConfiguration K hK)
459 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
460 (canonicalReggeHessian K hK))
461 (ξ : VertexPotential K) :
462 HasDerivAt
463 (fun t : ℝ =>
464 reggeActionRemainder K hK (canonicalReggeHessian K hK)
465 (linePotential K ξ t))
466 0 0 := by
467 -- ContDiffAt (1) at zeroPotential K gives differentiableAt → HasFDerivAt.
468 have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
469 (fun ξ' : VertexPotential K =>
470 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
471 (zeroPotential K) :=
472 canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
473 have hDiffR : DifferentiableAt ℝ
474 (fun ξ' : VertexPotential K =>
475 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
476 (zeroPotential K) :=
477 hContR.differentiableAt (by simp)
478 have hHasF : HasFDerivAt
479 (fun ξ' : VertexPotential K =>
480 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
481 (fderiv ℝ
482 (fun ξ' : VertexPotential K =>
483 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
484 (zeroPotential K))
485 (zeroPotential K) :=
486 hDiffR.hasFDerivAt
487 -- `fderiv = 0` from the remainder first-variation input.
488 have hFderiv0 :
489 fderiv ℝ
490 (fun ξ' : VertexPotential K =>
491 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
492 (zeroPotential K) = 0 :=
493 hFirst.remainder_firstVariation_zero
494 rw [hFderiv0] at hHasF
495 -- Rewrite (zeroPotential K) = (linePotential K ξ 0).
496 have hLine0 : zeroPotential K = linePotential K ξ 0 := (linePotential_zero K ξ).symm
497 rw [hLine0] at hHasF
498 -- Inner derivative: linePotential has derivative ξ.
499 have hInner : HasDerivAt (fun t : ℝ => linePotential K ξ t) ξ 0 :=
500 hasDerivAt_linePotential K ξ 0
501 -- Compose: HasDerivAt (R ∘ linePotential) ((fderiv R 0) ξ) 0.
502 have hComp := hHasF.comp_hasDerivAt 0 hInner
503 -- `(fderiv R 0) ξ = 0` since `fderiv R 0 = 0`.
504 -- After the `rw [hFderiv0]`, the outer derivative is the zero linear map; (0 : VP →L ℝ) ξ = 0.
505 simpa using hComp
506
507/-- `iteratedDerivWithin 0 R_line [0,1] 0 = 0`. -/
508theorem iteratedDerivWithin_zero_canonicalRemainderLine
509 (K : Triangulation3D) (hK : IncidenceConsistent K)
510 (ξ : VertexPotential K) :
511 iteratedDerivWithin 0
512 (fun t : ℝ =>
513 reggeActionRemainder K hK (canonicalReggeHessian K hK)
514 (linePotential K ξ t))
515 (Set.Icc (0 : ℝ) 1) 0 = 0 := by
516 rw [iteratedDerivWithin_zero]
517 exact canonicalRemainderLine_value_at_zero K hK ξ
518
519private theorem zero_mem_Icc_zero_one : (0 : ℝ) ∈ Set.Icc (0 : ℝ) 1 :=
520 ⟨le_refl 0, by norm_num⟩
521
522/-- `iteratedDerivWithin 1 R_line [0,1] 0 = 0` given the remainder
523first-variation input (which forces `fderiv R 0 = 0` and hence
524`deriv R_line 0 = 0` via the chain rule). -/
525theorem iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs
526 (K : Triangulation3D) (hK : IncidenceConsistent K)
527 (hFlat : FlatConfiguration K hK)
528 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
529 (canonicalReggeHessian K hK))
530 (ξ : VertexPotential K) :
531 iteratedDerivWithin 1
532 (fun t : ℝ =>
533 reggeActionRemainder K hK (canonicalReggeHessian K hK)
534 (linePotential K ξ t))
535 (Set.Icc (0 : ℝ) 1) 0 = 0 := by
536 have hContDiff :=
537 canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ
538 have h_iw_eq :
539 iteratedDerivWithin 1
540 (fun t : ℝ =>
541 reggeActionRemainder K hK (canonicalReggeHessian K hK)
542 (linePotential K ξ t))
543 (Set.Icc (0 : ℝ) 1) 0 =
544 iteratedDeriv 1
545 (fun t : ℝ =>
546 reggeActionRemainder K hK (canonicalReggeHessian K hK)
547 (linePotential K ξ t)) 0 := by
548 apply iteratedDerivWithin_eq_iteratedDeriv uniqueDiffOn_Icc_zero_one
549 _ zero_mem_Icc_zero_one
550 refine hContDiff.of_le ?_
551 exact (WithTop.coe_le_coe).mpr le_top
552 rw [h_iw_eq, iteratedDeriv_one]
553 -- deriv R_line 0 = 0 from HasDerivAt R_line 0 0.
554 exact (canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar
555 K hK hFlat hFirst ξ).deriv
556
557/-- `iteratedDerivWithin 2 R_line [0,1] 0 = 0` given the remainder
558second-variation input (`HasSecondDerivAt R_line 0 0`). -/
559theorem iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs
560 (K : Triangulation3D) (hK : IncidenceConsistent K)
561 (hFlat : FlatConfiguration K hK)
562 (hSecond : ReggeActionRemainderSecondVariationInput K hK)
563 (ξ : VertexPotential K) :
564 iteratedDerivWithin 2
565 (fun t : ℝ =>
566 reggeActionRemainder K hK (canonicalReggeHessian K hK)
567 (linePotential K ξ t))
568 (Set.Icc (0 : ℝ) 1) 0 = 0 := by
569 have hContDiff :=
570 canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ
571 have h_iw_eq :
572 iteratedDerivWithin 2
573 (fun t : ℝ =>
574 reggeActionRemainder K hK (canonicalReggeHessian K hK)
575 (linePotential K ξ t))
576 (Set.Icc (0 : ℝ) 1) 0 =
577 iteratedDeriv 2
578 (fun t : ℝ =>
579 reggeActionRemainder K hK (canonicalReggeHessian K hK)
580 (linePotential K ξ t)) 0 := by
581 apply iteratedDerivWithin_eq_iteratedDeriv uniqueDiffOn_Icc_zero_one
582 _ zero_mem_Icc_zero_one
583 refine hContDiff.of_le ?_
584 exact (WithTop.coe_le_coe).mpr le_top
585 rw [h_iw_eq]
586 -- iteratedDeriv 2 f x = deriv (deriv f) x.
587 rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ, iteratedDeriv_one]
588 -- HasSecondDerivAt R_line 0 0 unfolds to HasDerivAt (deriv R_line) 0 0,
589 -- which gives `deriv (deriv R_line) 0 = 0`.
590 have hSecondAt : HasSecondDerivAt
591 (fun t : ℝ =>
592 reggeActionRemainder K hK (canonicalReggeHessian K hK)
593 (linePotential K ξ t))
594 0 0 :=
595 hSecond.remainder_secondVariation_zero ξ
596 unfold HasSecondDerivAt at hSecondAt
597 exact hSecondAt.deriv
598
599/-- **CLOSURE: `CanonicalRemainderLineQuadraticTaylorZeroTarget`.**
600
601The degree-2 Taylor polynomial at zero of the line-restricted canonical
602remainder evaluates to zero at `t = 1`, given `FlatConfiguration` plus
603the remainder's first- and second-variation inputs. The radius `r = 1` is
604arbitrary (the property holds for all `ξ`). -/
605theorem canonicalRemainderLineQuadraticTaylorZero_of_jetInputs
606 (K : Triangulation3D) (hK : IncidenceConsistent K)
607 (hFlat : FlatConfiguration K hK)
608 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
609 (canonicalReggeHessian K hK))
610 (hSecond : ReggeActionRemainderSecondVariationInput K hK) :
611 CanonicalRemainderLineQuadraticTaylorZeroTarget K hK := by
612 refine ⟨1, by norm_num, ?_⟩
613 intro ξ _hξ
614 -- Expand `taylorWithinEval` of degree 2 as a sum of three iteratedDerivWithin.
615 rw [taylor_within_apply]
616 -- Sum over k ∈ {0, 1, 2}.
617 have h0 := iteratedDerivWithin_zero_canonicalRemainderLine K hK ξ
618 have h1 := iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs
619 K hK hFlat hFirst ξ
620 have h2 := iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs
621 K hK hFlat hSecond ξ
622 -- Each term in the sum vanishes since the iterated derivatives are zero.
623 simp [Finset.sum_range_succ, h0, h1, h2]
624
625/-- Constructor obtaining the remainder second-variation input from
626`FlatConfiguration` plus the directional Hessian theorem. (Wrapper.) -/
627theorem reggeActionRemainderSecondVariationInput_of_flat_directionalHessian
628 (K : Triangulation3D) (hK : IncidenceConsistent K)
629 (hFlat : FlatConfiguration K hK)
630 (hHessian : ReggeActionNonlinearHessianProof.NonlinearReggeDirectionalHessianTheorem K hK) :
631 ReggeActionRemainderSecondVariationInput K hK :=
632 ReggeActionNonlinearHessianProof.reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian
633 K hK hFlat hHessian
634
635/-- `CanonicalRemainderLineQuadraticTaylorZeroTarget` from `FlatConfiguration`,
636the remainder first-variation input, and the directional Hessian theorem. -/
637theorem canonicalRemainderLineQuadraticTaylorZero_of_flat_first_and_directionalHessian
638 (K : Triangulation3D) (hK : IncidenceConsistent K)
639 (hFlat : FlatConfiguration K hK)
640 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
641 (canonicalReggeHessian K hK))
642 (hHessian : ReggeActionNonlinearHessianProof.NonlinearReggeDirectionalHessianTheorem K hK) :
643 CanonicalRemainderLineQuadraticTaylorZeroTarget K hK :=
644 canonicalRemainderLineQuadraticTaylorZero_of_jetInputs K hK hFlat hFirst
645 (reggeActionRemainderSecondVariationInput_of_flat_directionalHessian
646 K hK hFlat hHessian)
647
648/-! ## §7. Decomposition of `CanonicalRemainderLineThirdDerivBoundTarget`
649
650The third-derivative bound on the line-restricted canonical remainder
651factors through two reductions:
652
653(a) the **chain-rule identity** for `iteratedDeriv 3 (R ∘ lineCLM ξ) t`
654 in terms of `iteratedFDeriv ℝ 3 R (t • ξ)` evaluated on three copies
655 of `ξ`, which yields the `‖ξ‖^3` scaling, and
656
657(b) the **local norm bound** on `‖iteratedFDeriv ℝ 3 R z‖` for `z` in a
658 neighborhood of the flat point, which yields the constant `M`.
659
660Both reductions hold by general Mathlib content (`iteratedFDeriv_comp_right`
661plus `ContinuousMultilinearMap.le_opNorm` for (a), and
662`ContDiffAt.continuousAt_iteratedFDeriv` for (b)). We expose them as named
663sub-targets and discharge `CanonicalRemainderLineThirdDerivBoundTarget` from
664their conjunction. Both sub-targets are now closed from `FlatConfiguration`
665below. -/
666
667/-- The continuous linear map `t ↦ t • ξ : ℝ →L[ℝ] VertexPotential K`. -/
668noncomputable def lineCLM (K : Triangulation3D) (ξ : VertexPotential K) :
669 ℝ →L[ℝ] VertexPotential K :=
670 ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℝ ℝ) ξ
671
672@[simp] theorem lineCLM_apply
673 (K : Triangulation3D) (ξ : VertexPotential K) (t : ℝ) :
674 lineCLM K ξ t = t • ξ := by
675 simp [lineCLM, ContinuousLinearMap.smulRight_apply]
676
677@[simp] theorem lineCLM_eq_linePotential
678 (K : Triangulation3D) (ξ : VertexPotential K) (t : ℝ) :
679 lineCLM K ξ t = linePotential K ξ t := by
680 rw [lineCLM_apply, ← linePotential_eq_smul]
681
682theorem lineCLM_one (K : Triangulation3D) (ξ : VertexPotential K) :
683 lineCLM K ξ 1 = ξ := by simp
684
685/-- The line-restricted canonical remainder equals the composition of `R` with
686`lineCLM K ξ`. -/
687theorem canonicalRemainder_line_eq_comp
688 (K : Triangulation3D) (hK : IncidenceConsistent K)
689 (ξ : VertexPotential K) :
690 (fun t : ℝ =>
691 reggeActionRemainder K hK (canonicalReggeHessian K hK)
692 (linePotential K ξ t)) =
693 (fun ξ' : VertexPotential K =>
694 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') ∘
695 (lineCLM K ξ) := by
696 funext t
697 show reggeActionRemainder K hK (canonicalReggeHessian K hK)
698 (linePotential K ξ t) =
699 reggeActionRemainder K hK (canonicalReggeHessian K hK) (lineCLM K ξ t)
700 rw [lineCLM_eq_linePotential]
701
702/-- Sub-target (a): the chain-rule pointwise bound, **localized** to a small
703ball of radius `ε` around `0` and the unit segment `[0, 1]`.
704
705Localization is necessary because the chain rule
706`iteratedFDeriv 3 (R ∘ g) t = (iteratedFDeriv 3 R (g t)).compContinuousLinearMap (fun _ => g)`
707holds globally only if `R` is C³ globally (which we don't have); within a
708neighborhood of `0` where `R` is C³, the within-set chain rule
709(`ContinuousLinearMap.iteratedFDerivWithin_comp_right`) plus
710`iteratedFDerivWithin_of_isOpen` upgrade to free-space `iteratedFDeriv`.
711
712The statement: there is some `ε > 0` such that, for all `ξ` with `‖ξ‖ < ε`
713and all `t ∈ [0, 1]`, the third iterated derivative of the line-restricted
714remainder at `t` is bounded by
715`‖iteratedFDeriv ℝ 3 R (t • ξ)‖ · ‖ξ‖³`. -/
716def CanonicalRemainderLineChainRuleBoundTarget
717 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
718 ∃ ε : ℝ, 0 < ε ∧
719 ∀ (ξ : VertexPotential K), ‖ξ‖ < ε →
720 ∀ t ∈ Set.Icc (0 : ℝ) 1,
721 |iteratedDeriv 3
722 (fun s : ℝ =>
723 reggeActionRemainder K hK (canonicalReggeHessian K hK)
724 (linePotential K ξ s)) t|
725 ≤ ‖iteratedFDeriv ℝ 3
726 (fun ξ' : VertexPotential K =>
727 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
728 (t • ξ)‖
729 * ‖ξ‖ ^ (3 : ℕ)
730
731/-- Sub-target (b): the local norm bound on the third Fréchet derivative of
732`R` in a neighborhood of the flat point. This is `ContDiffAt` plus
733`ContDiffAt.continuousAt_iteratedFDeriv`; we expose it as a named target so
734the third-deriv bound is theorem-grade conditional on it. -/
735def CanonicalRemainderIteratedFDerivLocalBoundTarget
736 (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
737 ∃ (δ M : ℝ), 0 < δ ∧ 0 ≤ M ∧
738 ∀ z : VertexPotential K, ‖z‖ < δ →
739 ‖iteratedFDeriv ℝ 3
740 (fun ξ' : VertexPotential K =>
741 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
742 z‖ ≤ M
743
744/-- **CLOSURE CONDITIONAL ON CHAIN-RULE + LOCAL NORM BOUND.**
745
746Given the chain-rule pointwise bound and the local norm bound on the third
747Fréchet derivative of `R`, the line-restricted third-derivative bound holds
748with the same `M` and `r := δ`, valid for all `‖ξ‖ < r` and all `t ∈ [0, 1]`.
749
750Proof: for `‖ξ‖ < δ` and `t ∈ [0, 1]`, the point `t • ξ` has norm
751`|t| · ‖ξ‖ ≤ ‖ξ‖ < δ`, so the local norm bound applies and yields
752`‖iteratedFDeriv ℝ 3 R (t • ξ)‖ ≤ M`. The chain-rule pointwise bound then
753gives `|iteratedDeriv 3 R_line t| ≤ M · ‖ξ‖³`. -/
754theorem canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm
755 (K : Triangulation3D) (hK : IncidenceConsistent K)
756 (hChain : CanonicalRemainderLineChainRuleBoundTarget K hK)
757 (hLocal : CanonicalRemainderIteratedFDerivLocalBoundTarget K hK) :
758 CanonicalRemainderLineThirdDerivBoundTarget K hK := by
759 rcases hLocal with ⟨δ, M, hδ, hM, hBound⟩
760 rcases hChain with ⟨εC, hεC, hChainBnd⟩
761 refine ⟨min δ εC, M, lt_min hδ hεC, hM, ?_⟩
762 intro ξ hξ t ht
763 have hξC : ‖ξ‖ < εC := lt_of_lt_of_le hξ (min_le_right _ _)
764 have hξL : ‖ξ‖ < δ := lt_of_lt_of_le hξ (min_le_left _ _)
765 -- Apply the localized chain-rule pointwise bound.
766 have hChainPt := hChainBnd ξ hξC t ht
767 -- Local norm bound at point `t • ξ`.
768 have h_tξ_norm : ‖t • ξ‖ < δ := by
769 have h_t_abs : |t| ≤ 1 := by
770 rw [abs_of_nonneg ht.1]; exact ht.2
771 rw [norm_smul, Real.norm_eq_abs]
772 calc |t| * ‖ξ‖ ≤ 1 * ‖ξ‖ := by
773 exact mul_le_mul_of_nonneg_right h_t_abs (norm_nonneg ξ)
774 _ = ‖ξ‖ := one_mul _
775 _ < δ := hξL
776 have h_local := hBound (t • ξ) h_tξ_norm
777 -- Combine: |iteratedDeriv 3 R_line t| ≤ ‖iteratedFDeriv 3 R (t • ξ)‖ · ‖ξ‖³ ≤ M · ‖ξ‖³.
778 calc |iteratedDeriv 3
779 (fun s : ℝ =>
780 reggeActionRemainder K hK (canonicalReggeHessian K hK)
781 (linePotential K ξ s)) t|
782 ≤ ‖iteratedFDeriv ℝ 3
783 (fun ξ' : VertexPotential K =>
784 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
785 (t • ξ)‖
786 * ‖ξ‖ ^ (3 : ℕ) := hChainPt
787 _ ≤ M * ‖ξ‖ ^ (3 : ℕ) := by
788 have hξ3 : 0 ≤ ‖ξ‖ ^ (3 : ℕ) := by positivity
789 exact mul_le_mul_of_nonneg_right h_local hξ3
790
791/-- **CLOSURE: `CanonicalRemainderIteratedFDerivLocalBoundTarget`.**
792
793The third Fréchet derivative of the canonical remainder is locally bounded
794at the flat point: by `ContDiffAt` and `ContDiffAt.continuousAt_iteratedFDeriv`,
795`iteratedFDeriv ℝ 3 R` is continuous at `0`, so `‖iteratedFDeriv ℝ 3 R z‖ < ‖0‖ + 1`
796for `z` close to `0`. We take `M := ‖iteratedFDeriv ℝ 3 R 0‖ + 1` and `δ` from
797the continuity δ-ε statement. -/
798theorem canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration
799 (K : Triangulation3D) (hK : IncidenceConsistent K)
800 (hFlat : FlatConfiguration K hK) :
801 CanonicalRemainderIteratedFDerivLocalBoundTarget K hK := by
802 -- ContDiffAt of R at zeroPotential at order ⊤.
803 have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
804 (fun ξ' : VertexPotential K =>
805 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
806 (zeroPotential K) :=
807 canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
808 -- iteratedFDeriv 3 R is continuous at zeroPotential K.
809 have hContAt :
810 ContinuousAt
811 (iteratedFDeriv ℝ 3
812 (fun ξ' : VertexPotential K =>
813 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ'))
814 (zeroPotential K) := by
815 refine hContR.continuousAt_iteratedFDeriv (k := 3) ?_
816 exact (WithTop.coe_le_coe).mpr le_top
817 -- Set the bound `M := ‖iteratedFDeriv 3 R 0‖ + 1`.
818 set M : ℝ := ‖iteratedFDeriv ℝ 3
819 (fun ξ' : VertexPotential K =>
820 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
821 (zeroPotential K)‖ + 1 with hM_def
822 have hM_nonneg : 0 ≤ M := by
823 have hpos : 0 ≤ ‖iteratedFDeriv ℝ 3
824 (fun ξ' : VertexPotential K =>
825 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
826 (zeroPotential K)‖ := norm_nonneg _
827 linarith
828 -- Continuity at zeroPotential K with tolerance 1.
829 rw [Metric.continuousAt_iff] at hContAt
830 obtain ⟨δ, hδ_pos, hδ⟩ := hContAt 1 (by norm_num : (0 : ℝ) < 1)
831 refine ⟨δ, M, hδ_pos, hM_nonneg, ?_⟩
832 intro z hz
833 -- ‖z - zeroPotential K‖ = ‖z‖ since zeroPotential K is the zero element.
834 have hz_dist : dist z (zeroPotential K) < δ := by
835 rw [dist_eq_norm]
836 have h_zp : (zeroPotential K) = (0 : VertexPotential K) := by
837 funext i; simp [zeroPotential]
838 rw [h_zp]
839 simpa using hz
840 -- Apply continuity bound.
841 have h_dist := hδ hz_dist
842 -- h_dist : dist (iteratedFDeriv 3 R z) (iteratedFDeriv 3 R 0) < 1
843 rw [dist_eq_norm] at h_dist
844 -- ‖A - B‖ < 1 implies ‖A‖ ≤ ‖B‖ + 1 = M.
845 have h_le : ‖iteratedFDeriv ℝ 3
846 (fun ξ' : VertexPotential K =>
847 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z‖
848 ≤ ‖iteratedFDeriv ℝ 3
849 (fun ξ' : VertexPotential K =>
850 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
851 (zeroPotential K)‖ + 1 := by
852 have h_tri := norm_sub_norm_le
853 (iteratedFDeriv ℝ 3
854 (fun ξ' : VertexPotential K =>
855 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z)
856 (iteratedFDeriv ℝ 3
857 (fun ξ' : VertexPotential K =>
858 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
859 (zeroPotential K))
860 linarith
861 exact h_le
862
863/-- **CLOSURE: `CanonicalRemainderLineChainRuleBoundTarget` (localized).**
864
865Within a small open ball `ball(0, ε)` around the flat point, the canonical
866remainder is `ContDiffOn ℝ 3` (from `canonicalRemainder_contDiffAt_zero_of_flatConfiguration`).
867For `ξ` with `‖ξ‖ < ε` and `t ∈ [0, 1]`, the point `t • ξ` lies in this ball,
868the within-set chain rule
869`ContinuousLinearMap.iteratedFDerivWithin_comp_right` applies, the within-set
870iterated Fréchet derivatives equal the free-space ones via
871`iteratedFDerivWithin_of_isOpen`, and the resulting expansion of
872`iteratedDeriv 3 (R ∘ lineCLM ξ) t` as
873`(iteratedFDeriv ℝ 3 R (t • ξ))(fun _ : Fin 3 => ξ)` is bounded by
874`‖iteratedFDeriv ℝ 3 R (t • ξ)‖ · ‖ξ‖³` via
875`ContinuousMultilinearMap.le_opNorm`. -/
876theorem canonicalRemainderLineChainRuleBound_of_flatConfiguration
877 (K : Triangulation3D) (hK : IncidenceConsistent K)
878 (hFlat : FlatConfiguration K hK) :
879 CanonicalRemainderLineChainRuleBoundTarget K hK := by
880 -- Step 1: extract a smooth nbhd of zeroPotential K.
881 have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
882 (fun ξ' : VertexPotential K =>
883 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
884 (zeroPotential K) :=
885 canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
886 have hContR3 : ContDiffAt ℝ (3 : ℕ∞)
887 (fun ξ' : VertexPotential K =>
888 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
889 (zeroPotential K) := by
890 refine hContR.of_le ?_
891 exact (WithTop.coe_le_coe).mpr le_top
892 -- Get a ContDiffOn nbhd from ContDiffAt.
893 rcases hContR3.contDiffOn (m := (3 : ℕ∞)) (le_refl _)
894 (by intro h; simp at h) with ⟨u, hu_nhds, hRu⟩
895 -- Refine to an open ball.
896 rcases Metric.mem_nhds_iff.mp hu_nhds with ⟨ε, hε_pos, hball⟩
897 -- ContDiffOn ℝ 3 R on ball(zeroPotential K, ε).
898 have hRball : ContDiffOn ℝ (3 : ℕ∞)
899 (fun ξ' : VertexPotential K =>
900 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
901 (Metric.ball (zeroPotential K) ε) :=
902 hRu.mono hball
903 -- Translate ball center to 0 (since zeroPotential K = 0 in VP K).
904 have hZP : (zeroPotential K) = (0 : VertexPotential K) := by
905 funext i; simp [zeroPotential]
906 -- Use ball at zero.
907 have hRball0 : ContDiffOn ℝ (3 : ℕ∞)
908 (fun ξ' : VertexPotential K =>
909 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
910 (Metric.ball (0 : VertexPotential K) ε) := by
911 rw [hZP] at hRball
912 exact hRball
913 refine ⟨ε, hε_pos, ?_⟩
914 intro ξ hξ t ht
915 -- Step 2: `t • ξ ∈ ball 0 ε`.
916 have h_t_abs : |t| ≤ 1 := by
917 rw [abs_of_nonneg ht.1]; exact ht.2
918 have h_tξ_in_ball : (t • ξ) ∈ Metric.ball (0 : VertexPotential K) ε := by
919 rw [Metric.mem_ball, dist_zero_right, norm_smul, Real.norm_eq_abs]
920 calc |t| * ‖ξ‖ ≤ 1 * ‖ξ‖ :=
921 mul_le_mul_of_nonneg_right h_t_abs (norm_nonneg ξ)
922 _ = ‖ξ‖ := one_mul _
923 _ < ε := hξ
924 -- Step 3: lineCLM ξ ⁻¹' (ball 0 ε) is open in ℝ.
925 have h_open_pre : IsOpen (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) :=
926 Metric.isOpen_ball.preimage (lineCLM K ξ).continuous
927 -- t ∈ preimage (since lineCLM K ξ t = t • ξ ∈ ball).
928 have h_t_in_pre : t ∈ lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε := by
929 rw [Set.mem_preimage, lineCLM_apply]; exact h_tξ_in_ball
930 -- UniqueDiffOn on preimage and on ball.
931 have h_uniq_ball : UniqueDiffOn ℝ (Metric.ball (0 : VertexPotential K) ε) :=
932 Metric.isOpen_ball.uniqueDiffOn
933 have h_uniq_pre : UniqueDiffOn ℝ
934 (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) :=
935 h_open_pre.uniqueDiffOn
936 -- Step 4: chain rule via `iteratedFDerivWithin_comp_right`.
937 have h_chain_within :
938 iteratedFDerivWithin ℝ 3
939 (fun s : ℝ =>
940 reggeActionRemainder K hK (canonicalReggeHessian K hK)
941 ((lineCLM K ξ) s))
942 (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) t =
943 (iteratedFDerivWithin ℝ 3
944 (fun ξ' : VertexPotential K =>
945 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
946 (Metric.ball (0 : VertexPotential K) ε)
947 (lineCLM K ξ t)).compContinuousLinearMap (fun _ : Fin 3 => lineCLM K ξ) := by
948 have h := (lineCLM K ξ).iteratedFDerivWithin_comp_right
949 (f := fun ξ' : VertexPotential K =>
950 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
951 (n := (3 : ℕ∞)) hRball0 h_uniq_ball h_uniq_pre h_tξ_in_ball
952 (i := 3) (le_refl _)
953 -- Adjust the LHS to use the function form rather than ∘.
954 convert h using 2
955 -- Step 5: convert iteratedFDerivWithin to iteratedFDeriv (open sets).
956 have ht_in_ball : lineCLM K ξ t ∈ Metric.ball (0 : VertexPotential K) ε := by
957 rw [lineCLM_apply]; exact h_tξ_in_ball
958 have h_within_eq_R :
959 iteratedFDerivWithin ℝ 3
960 (fun ξ' : VertexPotential K =>
961 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
962 (Metric.ball (0 : VertexPotential K) ε)
963 (lineCLM K ξ t) =
964 iteratedFDeriv ℝ 3
965 (fun ξ' : VertexPotential K =>
966 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
967 (lineCLM K ξ t) :=
968 iteratedFDerivWithin_of_isOpen 3 Metric.isOpen_ball ht_in_ball
969 have h_within_eq_comp :
970 iteratedFDerivWithin ℝ 3
971 (fun s : ℝ =>
972 reggeActionRemainder K hK (canonicalReggeHessian K hK)
973 ((lineCLM K ξ) s))
974 (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) t =
975 iteratedFDeriv ℝ 3
976 (fun s : ℝ =>
977 reggeActionRemainder K hK (canonicalReggeHessian K hK)
978 ((lineCLM K ξ) s)) t :=
979 iteratedFDerivWithin_of_isOpen 3 h_open_pre h_t_in_pre
980 -- Combine: free-space iteratedFDeriv chain-rule formula.
981 have h_chain_free :
982 iteratedFDeriv ℝ 3
983 (fun s : ℝ =>
984 reggeActionRemainder K hK (canonicalReggeHessian K hK)
985 ((lineCLM K ξ) s)) t =
986 (iteratedFDeriv ℝ 3
987 (fun ξ' : VertexPotential K =>
988 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
989 (lineCLM K ξ t)).compContinuousLinearMap (fun _ : Fin 3 => lineCLM K ξ) := by
990 rw [← h_within_eq_comp, h_chain_within, h_within_eq_R]
991 -- Step 6: rewrite the line-restricted remainder via `lineCLM`.
992 have h_eq_line :
993 (fun s : ℝ =>
994 reggeActionRemainder K hK (canonicalReggeHessian K hK)
995 (linePotential K ξ s)) =
996 (fun s : ℝ =>
997 reggeActionRemainder K hK (canonicalReggeHessian K hK)
998 ((lineCLM K ξ) s)) := by
999 funext s
1000 rw [lineCLM_eq_linePotential]
1001 -- Step 7: bound `|iteratedDeriv 3 R_line t|` using the chain-rule formula.
1002 rw [h_eq_line]
1003 -- iteratedDeriv 3 f t = (iteratedFDeriv ℝ 3 f t)(fun _ => 1).
1004 rw [iteratedDeriv]
1005 rw [h_chain_free]
1006 -- Now: |((iteratedFDeriv 3 R (lineCLM ξ t)).compCLM (fun _ => lineCLM ξ))(fun _ => 1)|
1007 -- = |(iteratedFDeriv 3 R (t • ξ))(fun _ => lineCLM ξ 1)|
1008 -- = |(iteratedFDeriv 3 R (t • ξ))(fun _ => ξ)|
1009 rw [ContinuousMultilinearMap.compContinuousLinearMap_apply]
1010 rw [lineCLM_apply]
1011 -- Goal: |(iteratedFDeriv 3 R (t • ξ))(fun _ => lineCLM ξ 1)| ≤ ‖...‖ · ‖ξ‖^3
1012 -- Use lineCLM_one to simplify (fun _ => lineCLM K ξ 1) = (fun _ => ξ).
1013 have h_lcm1 : (fun _ : Fin 3 => lineCLM K ξ 1) = (fun _ : Fin 3 => ξ) := by
1014 funext i; exact lineCLM_one K ξ
1015 rw [h_lcm1]
1016 -- Bound by `ContinuousMultilinearMap.le_opNorm`.
1017 have h_op := ContinuousMultilinearMap.le_opNorm
1018 (iteratedFDeriv ℝ 3
1019 (fun ξ' : VertexPotential K =>
1020 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1021 (t • ξ))
1022 (fun _ : Fin 3 => ξ)
1023 -- h_op : ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
1024 -- For m = const ξ on Fin 3, ∏ i, ‖ξ‖ = ‖ξ‖^3.
1025 have h_prod : (∏ _i : Fin 3, ‖ξ‖) = ‖ξ‖ ^ (3 : ℕ) := by
1026 rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin]
1027 -- Convert ‖_‖ to |_| for the real-valued LHS via `abs_eq_norm` on ℝ.
1028 have h_abs_eq : |(iteratedFDeriv ℝ 3
1029 (fun ξ' : VertexPotential K =>
1030 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1031 (t • ξ))
1032 (fun _ : Fin 3 => ξ)| =
1033 ‖(iteratedFDeriv ℝ 3
1034 (fun ξ' : VertexPotential K =>
1035 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1036 (t • ξ))
1037 (fun _ : Fin 3 => ξ)‖ := by
1038 rfl
1039 rw [h_abs_eq]
1040 calc ‖(iteratedFDeriv ℝ 3
1041 (fun ξ' : VertexPotential K =>
1042 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1043 (t • ξ))
1044 (fun _ : Fin 3 => ξ)‖
1045 ≤ ‖iteratedFDeriv ℝ 3
1046 (fun ξ' : VertexPotential K =>
1047 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1048 (t • ξ)‖ * (∏ _i : Fin 3, ‖ξ‖) := h_op
1049 _ = ‖iteratedFDeriv ℝ 3
1050 (fun ξ' : VertexPotential K =>
1051 reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
1052 (t • ξ)‖ * ‖ξ‖ ^ (3 : ℕ) := by rw [h_prod]
1053
1054/-- **CLOSURE OF `CanonicalRemainderLineThirdDerivBoundTarget`.**
1055
1056The third-derivative bound on the line-restricted canonical remainder
1057follows from `FlatConfiguration` alone, by combining the chain-rule bound
1058(`canonicalRemainderLineChainRuleBound_of_flatConfiguration`) with the local
1059norm bound (`canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration`)
1060through `canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm`. -/
1061theorem canonicalRemainderLineThirdDerivBound_of_flatConfiguration
1062 (K : Triangulation3D) (hK : IncidenceConsistent K)
1063 (hFlat : FlatConfiguration K hK) :
1064 CanonicalRemainderLineThirdDerivBoundTarget K hK :=
1065 canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm K hK
1066 (canonicalRemainderLineChainRuleBound_of_flatConfiguration K hK hFlat)
1067 (canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration K hK hFlat)
1068
1069/-- Composite: line-Taylor data target from the four sub-targets:
1070ContDiff, QuadraticTaylorZero, Chain-rule, and Local norm bound. All four are
1071closed in this module; this theorem remains as the explicit assembly point. -/
1072theorem canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm
1073 (K : Triangulation3D) (hK : IncidenceConsistent K)
1074 (hFlat : FlatConfiguration K hK)
1075 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1076 (canonicalReggeHessian K hK))
1077 (hSecond : ReggeActionRemainderSecondVariationInput K hK)
1078 (hChain : CanonicalRemainderLineChainRuleBoundTarget K hK)
1079 (hLocal : CanonicalRemainderIteratedFDerivLocalBoundTarget K hK) :
1080 CanonicalRemainderLineTaylorDataTarget K hK :=
1081 lineTaylorData_of_splitTargets K hK
1082 (canonicalRemainderLineContDiff_of_flatConfiguration K hK hFlat)
1083 (canonicalRemainderLineQuadraticTaylorZero_of_jetInputs K hK hFlat hFirst hSecond)
1084 (canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm K hK hChain hLocal)
1085
1086/-- **CASCADE CLOSURE: line-Taylor data from `FlatConfiguration` + jet inputs.**
1087
1088With the chain-rule bound now closed from `FlatConfiguration` alone
1089(`canonicalRemainderLineChainRuleBound_of_flatConfiguration`) and the local
1090norm bound also closed from `FlatConfiguration` alone
1091(`canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration`), the
1092line-Taylor data target closes from `FlatConfiguration` plus the remainder
1093first- and second-variation inputs. The latter two inputs are themselves
1094constructible from `FlatConfiguration` plus the directional Hessian theorem
1095(see `ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput`
1096and `reggeActionRemainderSecondVariationInput_of_flat_directionalHessian`). -/
1097theorem canonicalRemainderLineTaylorData_of_flat_and_remainderJets
1098 (K : Triangulation3D) (hK : IncidenceConsistent K)
1099 (hFlat : FlatConfiguration K hK)
1100 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1101 (canonicalReggeHessian K hK))
1102 (hSecond : ReggeActionRemainderSecondVariationInput K hK) :
1103 CanonicalRemainderLineTaylorDataTarget K hK :=
1104 canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm
1105 K hK hFlat hFirst hSecond
1106 (canonicalRemainderLineChainRuleBound_of_flatConfiguration K hK hFlat)
1107 (canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration K hK hFlat)
1108
1109/-- **CASCADE CLOSURE: cubic Taylor theorem from `FlatConfiguration` + jet
1110inputs.** -/
1111theorem nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets
1112 (K : Triangulation3D) (hK : IncidenceConsistent K)
1113 (hFlat : FlatConfiguration K hK)
1114 (hFirst : ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1115 (canonicalReggeHessian K hK))
1116 (hSecond : ReggeActionRemainderSecondVariationInput K hK) :
1117 NonlinearReggeCubicTaylorTheorem K hK :=
1118 nonlinearReggeCubicTaylorTheorem_of_lineTaylorData K hK
1119 (canonicalRemainderLineTaylorData_of_flat_and_remainderJets
1120 K hK hFlat hFirst hSecond)
1121
1122/-! ## §8. 1B-REM audit certificate
1123
1124The local analytic-remainder lane is closed at the generic finite
1125triangulation level: from `FlatConfiguration` plus the standard remainder
1126first- and second-variation inputs, Lean has the line-Taylor data target and
1127the nonlinear cubic Taylor theorem. This certificate is intentionally
1128theorem-valued, not a list of stale `Prop` targets. -/
1129
1130structure CanonicalRemainderAnalyticClosureCert
1131 (K : Triangulation3D) (hK : IncidenceConsistent K) where
1132 line_contDiff_from_flat :
1133 FlatConfiguration K hK →
1134 CanonicalRemainderLineContDiffTarget K hK
1135 line_quadratic_zero_from_jets :
1136 FlatConfiguration K hK →
1137 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1138 (canonicalReggeHessian K hK) →
1139 ReggeActionRemainderSecondVariationInput K hK →
1140 CanonicalRemainderLineQuadraticTaylorZeroTarget K hK
1141 line_chain_rule_bound_from_flat :
1142 FlatConfiguration K hK →
1143 CanonicalRemainderLineChainRuleBoundTarget K hK
1144 iteratedFDeriv3_local_bound_from_flat :
1145 FlatConfiguration K hK →
1146 CanonicalRemainderIteratedFDerivLocalBoundTarget K hK
1147 line_third_deriv_bound_from_flat :
1148 FlatConfiguration K hK →
1149 CanonicalRemainderLineThirdDerivBoundTarget K hK
1150 line_taylor_data_from_flat_and_jets :
1151 FlatConfiguration K hK →
1152 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1153 (canonicalReggeHessian K hK) →
1154 ReggeActionRemainderSecondVariationInput K hK →
1155 CanonicalRemainderLineTaylorDataTarget K hK
1156 cubic_taylor_from_flat_and_jets :
1157 FlatConfiguration K hK →
1158 ReggeActionFirstVariation.ReggeActionRemainderFirstVariationInput K hK
1159 (canonicalReggeHessian K hK) →
1160 ReggeActionRemainderSecondVariationInput K hK →
1161 NonlinearReggeCubicTaylorTheorem K hK
1162
1163def canonicalRemainderAnalyticClosureCert
1164 (K : Triangulation3D) (hK : IncidenceConsistent K) :
1165 CanonicalRemainderAnalyticClosureCert K hK where
1166 line_contDiff_from_flat := fun hFlat =>
1167 canonicalRemainderLineContDiff_of_flatConfiguration K hK hFlat
1168 line_quadratic_zero_from_jets := fun hFlat hFirst hSecond =>
1169 canonicalRemainderLineQuadraticTaylorZero_of_jetInputs K hK hFlat hFirst hSecond
1170 line_chain_rule_bound_from_flat := fun hFlat =>
1171 canonicalRemainderLineChainRuleBound_of_flatConfiguration K hK hFlat
1172 iteratedFDeriv3_local_bound_from_flat := fun hFlat =>
1173 canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration K hK hFlat
1174 line_third_deriv_bound_from_flat := fun hFlat =>
1175 canonicalRemainderLineThirdDerivBound_of_flatConfiguration K hK hFlat
1176 line_taylor_data_from_flat_and_jets := fun hFlat hFirst hSecond =>
1177 canonicalRemainderLineTaylorData_of_flat_and_remainderJets K hK hFlat hFirst hSecond
1178 cubic_taylor_from_flat_and_jets := fun hFlat hFirst hSecond =>
1179 nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets K hK hFlat hFirst hSecond
1180
1181end
1182
1183end ReggeActionCubicTaylorBound
1184end Geometry
1185end IndisputableMonolith
1186