IndisputableMonolith.Geometry.ReggeActionSecondVariation

   1import Mathlib
   2import IndisputableMonolith.Geometry.ReggeActionFirstVariation
   3
   4/-!
   5# Second Variation and Cubic Remainder of the Nonlinear Regge Action
   6
   7This module states the nonlinear second-variation and cubic-remainder targets
   8in a form that is usable now.  The lower-level calculation is the large
   9Cayley-Menger/arccos chain-rule expansion; until that calculation is fully
  10materialized, the required analytic facts live in named input structures.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Geometry
  15namespace ReggeActionSecondVariation
  16
  17open ReggeTriangulation3D
  18open ReggeHessian3D
  19open Triangulation3DConsistency
  20open ReggeActionConcrete
  21open ReggeActionSmoothness
  22open ReggeActionFirstVariation
  23
  24noncomputable section
  25
  26/-- The line through the flat potential in direction `ξ`. -/
  27def linePotential (K : Triangulation3D) (ξ : VertexPotential K) (t : ℝ) :
  28    VertexPotential K :=
  29  fun i => t * ξ i
  30
  31theorem linePotential_zero
  32    (K : Triangulation3D) (ξ : VertexPotential K) :
  33    linePotential K ξ 0 = zeroPotential K := by
  34  funext i
  35  simp [linePotential, zeroPotential]
  36
  37/-- A one-variable second derivative statement used for directional Hessian
  38comparisons. -/
  39def HasSecondDerivAt (f : ℝ → ℝ) (d2 x : ℝ) : Prop :=
  40  HasDerivAt (fun t : ℝ => deriv f t) d2 x
  41
  42theorem hessianQuadratic_linePotential
  43    (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ)
  44    (ξ : VertexPotential K) (t : ℝ) :
  45    hessianQuadratic H (linePotential K ξ t) =
  46      t ^ 2 * hessianQuadratic H ξ := by
  47  unfold hessianQuadratic linePotential
  48  rw [Finset.mul_sum]
  49  refine Finset.sum_congr rfl ?_
  50  intro i _
  51  rw [Finset.mul_sum]
  52  refine Finset.sum_congr rfl ?_
  53  intro j _
  54  ring
  55
  56theorem hessianQuadratic_along_line_hasSecondDerivAt_zero
  57    (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ)
  58    (ξ : VertexPotential K) :
  59    HasSecondDerivAt
  60      (fun t : ℝ => (1 / 2) * hessianQuadratic H (linePotential K ξ t))
  61      (hessianQuadratic H ξ) 0 := by
  62  unfold HasSecondDerivAt
  63  have hquad :
  64      (fun t : ℝ => (1 / 2) * hessianQuadratic H (linePotential K ξ t)) =
  65        fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2 := by
  66    funext t
  67    rw [hessianQuadratic_linePotential]
  68    ring
  69  rw [hquad]
  70  have hderiv :
  71      deriv (fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2) =
  72        fun t : ℝ => hessianQuadratic H ξ * t := by
  73    ext t
  74    have h :=
  75      ((hasDerivAt_id t).pow 2).const_mul (hessianQuadratic H ξ / 2)
  76    have h' : HasDerivAt
  77        (fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2)
  78        (hessianQuadratic H ξ * t) t := by
  79      simpa [id, two_mul, mul_comm, mul_left_comm, mul_assoc] using h
  80    exact h'.deriv
  81  rw [hderiv]
  82  simpa using (hasDerivAt_id 0).const_mul (hessianQuadratic H ξ)
  83
  84/-- The nonlinear Regge action restricted to a one-dimensional conformal
  85line through the flat potential. -/
  86def actionAlongLine
  87    (K : Triangulation3D) (hK : IncidenceConsistent K)
  88    (ξ : VertexPotential K) (t : ℝ) : ℝ :=
  89  reggeAction K hK (linePotential K ξ t)
  90
  91/-- The nonlinear action has the canonical incidence Hessian as its second
  92variation at the flat potential, tested on every conformal line. -/
  93def CanonicalHessianSecondVariationAtZero
  94    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  95  ∀ ξ : VertexPotential K,
  96    HasSecondDerivAt (actionAlongLine K hK ξ)
  97      (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0
  98
  99/-- Named second-variation input for the full nonlinear action. -/
 100structure ReggeActionSecondVariationInput
 101    (K : Triangulation3D) (hK : IncidenceConsistent K)
 102    (_h_flat : FlatConfiguration K hK) where
 103  canonical_secondVariation : CanonicalHessianSecondVariationAtZero K hK
 104
 105def reggeActionSecondVariationInput_of_directionalSecondVariation
 106    (K : Triangulation3D) (hK : IncidenceConsistent K)
 107    (h_flat : FlatConfiguration K hK)
 108    (hSecond : CanonicalHessianSecondVariationAtZero K hK) :
 109    ReggeActionSecondVariationInput K hK h_flat where
 110  canonical_secondVariation := hSecond
 111
 112/-- Phase-D second-variation theorem, conditional on the named nonlinear
 113second-variation input. -/
 114theorem reggeAction_secondVariation_eq_canonicalHessian
 115    (K : Triangulation3D) (hK : IncidenceConsistent K)
 116    (h_flat : FlatConfiguration K hK)
 117    (h_second : ReggeActionSecondVariationInput K hK h_flat) :
 118    CanonicalHessianSecondVariationAtZero K hK :=
 119  h_second.canonical_secondVariation
 120
 121/-- The canonical nonlinear remainder has zero second variation at the flat
 122potential. -/
 123def CanonicalRemainderSecondVariationZero
 124    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
 125  ∀ ξ : VertexPotential K,
 126    HasSecondDerivAt
 127      (fun t : ℝ =>
 128        reggeActionRemainder K hK (canonicalReggeHessian K hK)
 129          (linePotential K ξ t))
 130      0 0
 131
 132structure ReggeActionRemainderSecondVariationInput
 133    (K : Triangulation3D) (hK : IncidenceConsistent K) where
 134  remainder_secondVariation_zero :
 135    CanonicalRemainderSecondVariationZero K hK
 136
 137theorem reggeActionRemainder_secondVariation_zero
 138    (K : Triangulation3D) (hK : IncidenceConsistent K)
 139    (h_rem : ReggeActionRemainderSecondVariationInput K hK) :
 140    CanonicalRemainderSecondVariationZero K hK :=
 141  h_rem.remainder_secondVariation_zero
 142
 143/-- Local cubic bound for the canonical nonlinear Taylor remainder. -/
 144def LocalCubicRemainderBound
 145    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
 146  ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
 147    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
 148      ‖reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ‖ ≤
 149        C * ‖ξ‖ ^ (3 : ℕ)
 150
 151/-- Named Taylor-remainder input.  This is the exact place where Mathlib's
 152multivariate Taylor theorem, or an `IsBigO` fallback, should be connected. -/
 153structure ReggeActionCubicRemainderInput
 154    (K : Triangulation3D) (hK : IncidenceConsistent K)
 155    (_h_flat : FlatConfiguration K hK) where
 156  cubic_bound : LocalCubicRemainderBound K hK
 157
 158def reggeActionCubicRemainderInput_of_bound
 159    (K : Triangulation3D) (hK : IncidenceConsistent K)
 160    (h_flat : FlatConfiguration K hK)
 161    (hBound : LocalCubicRemainderBound K hK) :
 162    ReggeActionCubicRemainderInput K hK h_flat where
 163  cubic_bound := hBound
 164
 165/-- A strong but useful sanity constructor: if the canonical remainder is
 166identically zero, it satisfies the local cubic bound with constant zero. -/
 167def reggeActionCubicRemainderInput_of_identically_zero
 168    (K : Triangulation3D) (hK : IncidenceConsistent K)
 169    (h_flat : FlatConfiguration K hK)
 170    (hZero :
 171      ∀ ξ : VertexPotential K,
 172        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
 173    ReggeActionCubicRemainderInput K hK h_flat where
 174  cubic_bound := by
 175    refine ⟨1, 0, by norm_num, le_rfl, ?_⟩
 176    intro ξ _hξ
 177    rw [hZero ξ]
 178    simp
 179
 180/-- Phase-E cubic remainder theorem, conditional on the named Taylor input. -/
 181theorem reggeActionRemainder_cubic_bound
 182    (K : Triangulation3D) (hK : IncidenceConsistent K)
 183    (h_flat : FlatConfiguration K hK)
 184    (h_cubic : ReggeActionCubicRemainderInput K hK h_flat) :
 185    LocalCubicRemainderBound K hK :=
 186  h_cubic.cubic_bound
 187
 188end
 189
 190end ReggeActionSecondVariation
 191end Geometry
 192end IndisputableMonolith
 193