IndisputableMonolith.Geometry.CayleyMengerDerivatives
IndisputableMonolith/Geometry/CayleyMengerDerivatives.lean · 368 lines · 32 declarations
show as:
view math explainer →
1import Mathlib.Data.Real.Basic
2import Mathlib.Analysis.Calculus.ContDiff.Basic
3import Mathlib.Analysis.Calculus.ContDiff.Operations
4import Mathlib.Analysis.Calculus.Deriv.Basic
5import Mathlib.Analysis.Calculus.Deriv.Add
6import Mathlib.Analysis.Calculus.Deriv.Mul
7import Mathlib.Analysis.Calculus.Deriv.Pow
8import Mathlib.Analysis.Calculus.FDeriv.Basic
9import IndisputableMonolith.Geometry.CayleyMengerPolynomial
10
11/-!
12# Partial Derivatives of the Cayley-Menger Polynomial
13
14This module computes the six partial derivatives `∂CM_3/∂a_i` of the
15Cayley-Menger polynomial as explicit polynomial functions of the squared
16edge lengths. The central theorem is the polynomial Taylor identity for
17`cm3 (a + h)`, which exposes the gradient, quadratic term, and cubic
18remainder directly. From that identity we derive a uniform
19single-coordinate update formula and partial derivative API.
20
21## Why this matters
22
23The Regge second-variation matrix `M_ij` we ultimately compare to
24`area(f_ij)` is built from these partial derivatives via the chain rule
25through the conformal edge ansatz. Formal differentiability of `cm3` is
26already established in
27`CayleyMengerPolynomial.cm3_contDiff`. The contribution of *this*
28module is the explicit closed-form gradient.
29
30## Edge convention
31
32Same as in `CayleyMengerPolynomial.lean`:
33 edge 0 = (0,1), edge 1 = (0,2), edge 2 = (0,3),
34 edge 3 = (1,2), edge 4 = (1,3), edge 5 = (2,3).
35-/
36
37namespace IndisputableMonolith
38namespace Geometry
39namespace CayleyMengerDerivatives
40
41open CayleyMengerPolynomial
42
43noncomputable section
44
45/-! ## §1. Closed-form gradient
46
47Each partial of the polynomial
48
49```
50CM_3 = 2 · [ α·ν·(β+γ+λ+μ−α−ν)
51 + β·μ·(α+γ+λ+ν−β−μ)
52 + γ·λ·(α+β+μ+ν−γ−λ)
53 − α·β·λ − α·γ·μ − β·γ·ν − λ·μ·ν ]
54```
55
56is a quadratic polynomial in the six squared edge lengths. We list each
57partial in fully expanded form for downstream use.
58-/
59
60/-- Partial derivative of `cm3` with respect to `a 0` (= α = squared edge (0,1)). -/
61def cm3_partial0 (a : SqEdges) : ℝ :=
62 2 * ( a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5) - a 0 * a 5
63 + a 1 * a 4 + a 2 * a 3
64 - a 1 * a 3 - a 2 * a 4 )
65
66/-- Partial derivative of `cm3` with respect to `a 1` (= β = squared edge (0,2)). -/
67def cm3_partial1 (a : SqEdges) : ℝ :=
68 2 * ( a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4) - a 1 * a 4
69 + a 0 * a 5 + a 2 * a 3
70 - a 0 * a 3 - a 2 * a 5 )
71
72/-- Partial derivative of `cm3` with respect to `a 2` (= γ = squared edge (0,3)). -/
73def cm3_partial2 (a : SqEdges) : ℝ :=
74 2 * ( a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3) - a 2 * a 3
75 + a 0 * a 5 + a 1 * a 4
76 - a 0 * a 4 - a 1 * a 5 )
77
78/-- Partial derivative of `cm3` with respect to `a 3` (= λ = squared edge (1,2)). -/
79def cm3_partial3 (a : SqEdges) : ℝ :=
80 2 * ( a 2 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3) - a 2 * a 3
81 + a 0 * a 5 + a 1 * a 4
82 - a 0 * a 1 - a 4 * a 5 )
83
84/-- Partial derivative of `cm3` with respect to `a 4` (= μ = squared edge (1,3)). -/
85def cm3_partial4 (a : SqEdges) : ℝ :=
86 2 * ( a 1 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4) - a 1 * a 4
87 + a 0 * a 5 + a 2 * a 3
88 - a 0 * a 2 - a 3 * a 5 )
89
90/-- Partial derivative of `cm3` with respect to `a 5` (= ν = squared edge (2,3)). -/
91def cm3_partial5 (a : SqEdges) : ℝ :=
92 2 * ( a 0 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5) - a 0 * a 5
93 + a 1 * a 4 + a 2 * a 3
94 - a 1 * a 2 - a 3 * a 4 )
95
96/-- The gradient packaged as a function `SqEdges → SqEdges`. At each
97basepoint `a`, this is the vector of partial derivatives. -/
98def cm3_grad (a : SqEdges) : SqEdges := fun i =>
99 match i with
100 | ⟨0, _⟩ => cm3_partial0 a
101 | ⟨1, _⟩ => cm3_partial1 a
102 | ⟨2, _⟩ => cm3_partial2 a
103 | ⟨3, _⟩ => cm3_partial3 a
104 | ⟨4, _⟩ => cm3_partial4 a
105 | ⟨5, _⟩ => cm3_partial5 a
106 | ⟨n+6, h⟩ => absurd h (by omega)
107
108/-! ## §3. Polynomial Taylor expansion of `cm3 (a + h) − cm3 a`
109
110Rather than repeat the 1-D `HasDerivAt` proof six times, we exhibit
111the full Taylor polynomial of `cm3` around any base point `a`:
112
113```
114cm3 (a + h) − cm3 a = ⟨grad cm3 a, h⟩ + Q(a, h) + C(h)
115```
116
117where `Q` is degree 2 in `h` and `C` is degree 3 in `h` (with no `a`
118dependence). Once this algebraic identity is established by `ring`,
119the Fréchet derivative of `cm3` at `a` is the linear functional
120`h ↦ ⟨grad cm3 a, h⟩`.
121
122This algebraic identity is the content of the partial-derivative
123formulas; the single-coordinate update formula below is the input for
124the derivative and Hessian APIs. -/
125
126/-- The quadratic-in-`h` correction in the Taylor expansion of
127`cm3 (a + h)` around `a`. Explicitly written. -/
128def cm3_quadratic (a h : SqEdges) : ℝ :=
129 2 * ( h 0 * h 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
130 + a 0 * h 5 * (h 1 + h 2 + h 3 + h 4 - h 0 - h 5)
131 + h 0 * a 5 * (h 1 + h 2 + h 3 + h 4 - h 0 - h 5)
132 + h 1 * h 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
133 + a 1 * h 4 * (h 0 + h 2 + h 3 + h 5 - h 1 - h 4)
134 + h 1 * a 4 * (h 0 + h 2 + h 3 + h 5 - h 1 - h 4)
135 + h 2 * h 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
136 + a 2 * h 3 * (h 0 + h 1 + h 4 + h 5 - h 2 - h 3)
137 + h 2 * a 3 * (h 0 + h 1 + h 4 + h 5 - h 2 - h 3)
138 - a 0 * h 1 * h 3 - h 0 * a 1 * h 3 - h 0 * h 1 * a 3
139 - a 0 * h 2 * h 4 - h 0 * a 2 * h 4 - h 0 * h 2 * a 4
140 - a 1 * h 2 * h 5 - h 1 * a 2 * h 5 - h 1 * h 2 * a 5
141 - a 3 * h 4 * h 5 - h 3 * a 4 * h 5 - h 3 * h 4 * a 5 )
142
143/-- The cubic-in-`h` correction (independent of `a`). -/
144def cm3_cubic (h : SqEdges) : ℝ :=
145 2 * ( h 0 * h 5 * (h 1 + h 2 + h 3 + h 4 - h 0 - h 5)
146 + h 1 * h 4 * (h 0 + h 2 + h 3 + h 5 - h 1 - h 4)
147 + h 2 * h 3 * (h 0 + h 1 + h 4 + h 5 - h 2 - h 3)
148 - h 0 * h 1 * h 3
149 - h 0 * h 2 * h 4
150 - h 1 * h 2 * h 5
151 - h 3 * h 4 * h 5 )
152
153/-- The "linear in `h`" gradient pairing:
154`⟨grad cm3 a, h⟩ = Σ_i (cm3_partial_i a) · h_i`. -/
155def cm3_linear (a h : SqEdges) : ℝ :=
156 cm3_partial0 a * h 0 + cm3_partial1 a * h 1 + cm3_partial2 a * h 2
157 + cm3_partial3 a * h 3 + cm3_partial4 a * h 4 + cm3_partial5 a * h 5
158
159/-- **Polynomial Taylor identity** (algebraic):
160
161`cm3 (a + h) = cm3 a + cm3_linear a h + cm3_quadratic a h + cm3_cubic h`. -/
162theorem cm3_taylor (a h : SqEdges) :
163 cm3 (fun i => a i + h i) =
164 cm3 a + cm3_linear a h + cm3_quadratic a h + cm3_cubic h := by
165 unfold cm3 cm3_linear cm3_partial0 cm3_partial1 cm3_partial2
166 cm3_partial3 cm3_partial4 cm3_partial5
167 cm3_quadratic cm3_cubic
168 ring
169
170/-- The single-coordinate perturbation: `singlePerturb i t` is the
171`SqEdges`-valued function that is `t` at index `i` and zero elsewhere. -/
172def singlePerturb (i : Fin 6) (t : ℝ) : SqEdges :=
173 fun j => if j = i then t else 0
174
175theorem singlePerturb_at (i : Fin 6) (t : ℝ) :
176 singlePerturb i t i = t := by
177 unfold singlePerturb; simp
178
179theorem singlePerturb_ne (i j : Fin 6) (h : j ≠ i) (t : ℝ) :
180 singlePerturb i t j = 0 := by
181 unfold singlePerturb; simp [h]
182
183/-- A specialised corollary of the Taylor identity: when only the
184`i`-th coordinate is perturbed, the formula collapses to the 1-D
185restriction of `cm3` along that coordinate. This is what feeds the
186six per-edge partial-derivative theorems. -/
187theorem cm3_update_taylor (a : SqEdges) (i : Fin 6) (t : ℝ) :
188 cm3 (Function.update a i (a i + t)) =
189 cm3 a + (cm3_grad a i) * t
190 + cm3_quadratic a (singlePerturb i t) + cm3_cubic (singlePerturb i t) := by
191 have hpt : (fun j : Fin 6 => a j + (singlePerturb i t) j)
192 = Function.update a i (a i + t) := by
193 funext j
194 by_cases hij : j = i
195 · subst hij
196 simp [singlePerturb_at]
197 · have h1 : (singlePerturb i t) j = 0 := singlePerturb_ne i j hij t
198 have h2 : Function.update a i (a i + t) j = a j := by
199 simp [Function.update, hij]
200 rw [h1, h2]
201 ring
202 have h := cm3_taylor a (singlePerturb i t)
203 rw [hpt] at h
204 rw [h]
205 have hlin : cm3_linear a (singlePerturb i t) = cm3_grad a i * t := by
206 unfold cm3_linear cm3_grad singlePerturb
207 fin_cases i <;> simp [cm3_partial0, cm3_partial1, cm3_partial2,
208 cm3_partial3, cm3_partial4, cm3_partial5]
209 linarith [hlin]
210
211/-! ## §4. Closed-form quadratic and cubic single-coordinate corrections
212
213The Taylor identity says that the correction `cm3_quadratic a
214(singlePerturb i t) + cm3_cubic (singlePerturb i t)` is a polynomial
215`α(a, i) t² + β(a, i) t³` in `t` with no constant or linear-in-`t`
216term. We compute the explicit `α, β` per edge `i` so that the per-edge
217partial-derivative theorems follow uniformly. -/
218
219/-- Quadratic-in-`t` coefficient of the single-coordinate correction. -/
220def cm3_quadratic_coeff : Fin 6 → SqEdges → ℝ
221 | 0, a => -2 * a 5
222 | 1, a => -2 * a 4
223 | 2, a => -2 * a 3
224 | 3, a => -2 * a 2
225 | 4, a => -2 * a 1
226 | 5, a => -2 * a 0
227
228/-- Cubic-in-`t` coefficient of the single-coordinate correction. In each
229case there is no `t³` contribution because the cm3 polynomial is degree 2 in
230each *individual* squared-edge coordinate. -/
231def cm3_cubic_coeff : Fin 6 → ℝ := fun _ => 0
232
233theorem cm3_quadratic_singlePerturb (a : SqEdges) (i : Fin 6) (t : ℝ) :
234 cm3_quadratic a (singlePerturb i t) =
235 cm3_quadratic_coeff i a * t ^ 2 := by
236 unfold cm3_quadratic singlePerturb cm3_quadratic_coeff
237 fin_cases i <;> simp <;> ring
238
239theorem cm3_cubic_singlePerturb (i : Fin 6) (t : ℝ) :
240 cm3_cubic (singlePerturb i t) = cm3_cubic_coeff i * t ^ 3 := by
241 unfold cm3_cubic singlePerturb cm3_cubic_coeff
242 fin_cases i <;> simp
243
244/-- Combined polynomial form of the Taylor expansion in single-coordinate
245direction:
246
247```
248cm3 (a.update i (a i + t))
249 = cm3 a + cm3_grad(a)(i) · t + cm3_quadratic_coeff i a · t² + cm3_cubic_coeff i · t³
250```
251-/
252theorem cm3_update_polyform (a : SqEdges) (i : Fin 6) (t : ℝ) :
253 cm3 (Function.update a i (a i + t)) =
254 cm3 a + cm3_grad a i * t
255 + cm3_quadratic_coeff i a * t ^ 2
256 + cm3_cubic_coeff i * t ^ 3 := by
257 rw [cm3_update_taylor a i t]
258 rw [cm3_quadratic_singlePerturb, cm3_cubic_singlePerturb]
259
260/-! ## §5. Derivative and Hessian API
261
262The update formula writes each one-coordinate restriction of `cm3` as a
263shifted cubic polynomial. Since `cm3_cubic_coeff = 0`, it is actually
264quadratic in each individual squared-edge coordinate. -/
265
266/-- Derivative of a shifted cubic polynomial at its base point. -/
267private theorem hasDerivAt_shifted_cubic (A B C D x₀ : ℝ) :
268 HasDerivAt (fun x : ℝ => A + B * (x - x₀) + C * (x - x₀) ^ 2
269 + D * (x - x₀) ^ 3) B x₀ := by
270 have hx : HasDerivAt (fun x : ℝ => x - x₀) (1 : ℝ) x₀ := by
271 simpa using (hasDerivAt_id x₀).sub_const x₀
272 have hconst : HasDerivAt (fun _ : ℝ => A) (0 : ℝ) x₀ := hasDerivAt_const x₀ A
273 have hlin : HasDerivAt (fun x : ℝ => B * (x - x₀)) B x₀ := by
274 have := hx.const_mul B
275 simpa using this
276 have hsq_raw := hx.pow 2
277 have hsq : HasDerivAt (fun x : ℝ => (x - x₀) ^ 2) (0 : ℝ) x₀ := by
278 simpa using hsq_raw
279 have hquad : HasDerivAt (fun x : ℝ => C * (x - x₀) ^ 2) (0 : ℝ) x₀ := by
280 have := hsq.const_mul C
281 simpa using this
282 have hcb_raw := hx.pow 3
283 have hcb : HasDerivAt (fun x : ℝ => (x - x₀) ^ 3) (0 : ℝ) x₀ := by
284 simpa using hcb_raw
285 have hcubic : HasDerivAt (fun x : ℝ => D * (x - x₀) ^ 3) (0 : ℝ) x₀ := by
286 have := hcb.const_mul D
287 simpa using this
288 have htotal := ((hconst.add hlin).add hquad).add hcubic
289 simpa using htotal
290
291/-- Uniform one-coordinate derivative of the Cayley-Menger polynomial.
292The derivative of `t ↦ cm3 (a.update i t)` at `t = a i` is the `i`th
293closed-form gradient entry. -/
294theorem hasDerivAt_cm3_grad (a : SqEdges) (i : Fin 6) :
295 HasDerivAt (fun t : ℝ => cm3 (Function.update a i t)) (cm3_grad a i) (a i) := by
296 have hfun :
297 (fun t : ℝ => cm3 (Function.update a i t)) =
298 (fun t : ℝ => cm3 a + cm3_grad a i * (t - a i)
299 + cm3_quadratic_coeff i a * (t - a i) ^ 2
300 + cm3_cubic_coeff i * (t - a i) ^ 3) := by
301 funext t
302 have h := cm3_update_polyform a i (t - a i)
303 have hbase : a i + (t - a i) = t := by ring
304 rw [hbase] at h
305 simpa using h
306 rw [hfun]
307 exact hasDerivAt_shifted_cubic (cm3 a) (cm3_grad a i)
308 (cm3_quadratic_coeff i a) (cm3_cubic_coeff i) (a i)
309
310/-- The closed-form `cm3_partial0` is the derivative of `t ↦ cm3 (a.update 0 t)`
311at `t = a 0`. -/
312theorem hasDerivAt_cm3_partial0 (a : SqEdges) :
313 HasDerivAt (fun t : ℝ => cm3 (Function.update a 0 t)) (cm3_partial0 a) (a 0) := by
314 simpa [cm3_grad] using hasDerivAt_cm3_grad a 0
315
316theorem hasDerivAt_cm3_partial1 (a : SqEdges) :
317 HasDerivAt (fun t : ℝ => cm3 (Function.update a 1 t)) (cm3_partial1 a) (a 1) := by
318 simpa [cm3_grad] using hasDerivAt_cm3_grad a 1
319
320theorem hasDerivAt_cm3_partial2 (a : SqEdges) :
321 HasDerivAt (fun t : ℝ => cm3 (Function.update a 2 t)) (cm3_partial2 a) (a 2) := by
322 simpa [cm3_grad] using hasDerivAt_cm3_grad a 2
323
324theorem hasDerivAt_cm3_partial3 (a : SqEdges) :
325 HasDerivAt (fun t : ℝ => cm3 (Function.update a 3 t)) (cm3_partial3 a) (a 3) := by
326 simpa [cm3_grad] using hasDerivAt_cm3_grad a 3
327
328theorem hasDerivAt_cm3_partial4 (a : SqEdges) :
329 HasDerivAt (fun t : ℝ => cm3 (Function.update a 4 t)) (cm3_partial4 a) (a 4) := by
330 simpa [cm3_grad] using hasDerivAt_cm3_grad a 4
331
332theorem hasDerivAt_cm3_partial5 (a : SqEdges) :
333 HasDerivAt (fun t : ℝ => cm3 (Function.update a 5 t)) (cm3_partial5 a) (a 5) := by
334 simpa [cm3_grad] using hasDerivAt_cm3_grad a 5
335
336/-- Hessian diagonal entries with respect to the squared-edge coordinates.
337Since `cm3 (a.update i (a i + t))` has quadratic coefficient
338`cm3_quadratic_coeff i a`, the second derivative in coordinate `i` is
339`2 * cm3_quadratic_coeff i a`. -/
340def cm3_hessianDiag (a : SqEdges) (i : Fin 6) : ℝ :=
341 2 * cm3_quadratic_coeff i a
342
343/-- The Fréchet derivative of `cm3` at `a`, as Mathlib's canonical
344continuous linear map. The coordinate formulas above identify its
345single-coordinate directional derivatives. -/
346def cm3GradientCLM (a : SqEdges) : SqEdges →L[ℝ] ℝ :=
347 fderiv ℝ cm3 a
348
349/-- `cm3GradientCLM` really is the Fréchet derivative of `cm3`. -/
350theorem hasFDerivAt_cm3 (a : SqEdges) :
351 HasFDerivAt cm3 (cm3GradientCLM a) a := by
352 unfold cm3GradientCLM
353 exact ((cm3_contDiff 1).differentiable_one a).hasFDerivAt
354
355/-- The one-coordinate update polynomial, rewritten in Hessian form. -/
356theorem cm3_update_hessianForm (a : SqEdges) (i : Fin 6) (t : ℝ) :
357 cm3 (Function.update a i (a i + t)) =
358 cm3 a + cm3_grad a i * t + (cm3_hessianDiag a i / 2) * t ^ 2 := by
359 rw [cm3_update_polyform]
360 unfold cm3_hessianDiag cm3_cubic_coeff
361 ring
362
363end
364
365end CayleyMengerDerivatives
366end Geometry
367end IndisputableMonolith
368