Geometry Regge Action Cubic Taylor Bound Regge Action Remainder Second Variation

/-- Exact Taylor theorem needed for the nonlinear Regge remainder.  This is
the finite-dimensional third-order Taylor estimate specialized to the canonical
Regge remainder. -/
def NonlinearReggeCubicTaylorTheorem
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  LocalCubicRemainderBound K hK

theorem canonicalRemainderLineContDiff_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    CanonicalRemainderLineContDiffTarget K hK := by
  let R : VertexPotential K → ℝ :=
    fun ξ => reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ
  have hR : ContDiffAt ℝ (⊤ : ℕ∞) R (zeroPotential K) := by
    simpa [R] using canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
  have hle : ((3 : ℕ∞) : WithTop ℕ∞) ≤ ((⊤ : ℕ∞) : WithTop ℕ∞) := by
    exact WithTop.coe_le_coe.2 le_top
  rcases hR.contDiffOn (m := (3 : ℕ∞)) hle (by intro h; simp at h) with
    ⟨u, hu, hRu⟩
  rcases Metric.mem_nhds_iff.mp hu with ⟨eps, heps, hball⟩
  refine ⟨eps, heps, ?_⟩
  intro ξ hξ
  have hline : ContDiffOn ℝ (3 : ℕ∞)
      (fun t : ℝ => linePotential K ξ t) (Set.Icc (0 : ℝ) 1) := by
    rw [contDiffOn_pi]
    intro i
    unfold linePotential
    fun_prop
  have hmaps : Set.MapsTo (fun t : ℝ => linePotential K ξ t)
      (Set.Icc (0 : ℝ) 1) u := by
    intro t ht
    apply hball
    rw [Metric.mem_ball, dist_eq_norm]
    have hsub : linePotential K ξ t - zeroPotential K = linePotential K ξ t := by
      funext i
      simp [zeroPotential]
    rw [hsub]
    exact lt_of_le_of_lt (norm_linePotential_le_of_mem_Icc_zero_one K ξ ht) hξ
  have hcomp := hRu.comp hline hmaps
  simpa [R, Function.comp_def] using hcomp

/-- **CLOSURE: `CanonicalRemainderLineChainRuleBoundTarget` (localized).**

Within a small open ball `ball(0, ε)` around the flat point, the canonical
remainder is `ContDiffOn ℝ 3` (from `canonicalRemainder_contDiffAt_zero_of_flatConfiguration`).
For `ξ` with `‖ξ‖ < ε` and `t ∈ [0, 1]`, the point `t • ξ` lies in this ball,
the within-set chain rule
`ContinuousLinearMap.iteratedFDerivWithin_comp_right` applies, the within-set
iterated Fréchet derivatives equal the free-space ones via
`iteratedFDerivWithin_of_isOpen`, and the resulting expansion of
`iteratedDeriv 3 (R ∘ lineCLM ξ) t` as
`(iteratedFDeriv ℝ 3 R (t • ξ))(fun _ : Fin 3 => ξ)` is bounded by
`‖iteratedFDeriv ℝ 3 R (t • ξ)‖ · ‖ξ‖³` via
`ContinuousMultilinearMap.le_opNorm`. -/
theorem canonicalRemainderLineChainRuleBound_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    CanonicalRemainderLineChainRuleBoundTarget K hK := by
  -- Step 1: extract a smooth nbhd of zeroPotential K.
  have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (zeroPotential K) :=
    canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
  have hContR3 : ContDiffAt ℝ (3 : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (zeroPotential K) := by
    refine hContR.of_le ?_
    exact (WithTop.coe_le_coe).mpr le_top
  -- Get a ContDiffOn nbhd from ContDiffAt.
  rcases hContR3.contDiffOn (m := (3 : ℕ∞)) (le_refl _)
      (by intro h; simp at h) with ⟨u, hu_nhds, hRu⟩
  -- Refine to an open ball.
  rcases Metric.mem_nhds_iff.mp hu_nhds with ⟨ε, hε_pos, hball⟩
  -- ContDiffOn ℝ 3 R on ball(zeroPotential K, ε).
  have hRball : ContDiffOn ℝ (3 : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (Metric.ball (zeroPotential K) ε) :=
    hRu.mono hball
  -- Translate ball center to 0 (since zeroPotential K = 0 in VP K).
  have hZP : (zeroPotential K) = (0 : VertexPotential K) := by
    funext i; simp [zeroPotential]
  -- Use ball at zero.
  have hRball0 : ContDiffOn ℝ (3 : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (Metric.ball (0 : VertexPotential K) ε) := by
    rw [hZP] at hRball
    exact hRball
  refine ⟨ε, hε_pos, ?_⟩
  intro ξ hξ t ht
  -- Step 2: `t • ξ ∈ ball 0 ε`.
  have h_t_abs : |t| ≤ 1 := by
    rw [abs_of_nonneg ht.1]; exact ht.2
  have h_tξ_in_ball : (t • ξ) ∈ Metric.ball (0 : VertexPotential K) ε := by
    rw [Metric.mem_ball, dist_zero_right, norm_smul, Real.norm_eq_abs]
    calc |t| * ‖ξ‖ ≤ 1 * ‖ξ‖ :=
          mul_le_mul_of_nonneg_right h_t_abs (norm_nonneg ξ)
      _ = ‖ξ‖ := one_mul _
      _ < ε := hξ
  -- Step 3: lineCLM ξ ⁻¹' (ball 0 ε) is open in ℝ.
  have h_open_pre : IsOpen (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) :=
    Metric.isOpen_ball.preimage (lineCLM K ξ).continuous
  -- t ∈ preimage (since lineCLM K ξ t = t • ξ ∈ ball).
  have h_t_in_pre : t ∈ lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε := by
    rw [Set.mem_preimage, lineCLM_apply]; exact h_tξ_in_ball
  -- UniqueDiffOn on preimage and on ball.
  have h_uniq_ball : UniqueDiffOn ℝ (Metric.ball (0 : VertexPotential K) ε) :=
    Metric.isOpen_ball.uniqueDiffOn
  have h_uniq_pre : UniqueDiffOn ℝ
      (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) :=
    h_open_pre.uniqueDiffOn
  -- Step 4: chain rule via `iteratedFDerivWithin_comp_right`.
  have h_chain_within :
      iteratedFDerivWithin ℝ 3
        (fun s : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            ((lineCLM K ξ) s))
        (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) t =
        (iteratedFDerivWithin ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (Metric.ball (0 : VertexPotential K) ε)
          (lineCLM K ξ t)).compContinuousLinearMap (fun _ : Fin 3 => lineCLM K ξ) := by
    have h := (lineCLM K ξ).iteratedFDerivWithin_comp_right
      (f := fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (n := (3 : ℕ∞)) hRball0 h_uniq_ball h_uniq_pre h_tξ_in_ball
      (i := 3) (le_refl _)
    -- Adjust the LHS to use the function form rather than ∘.
    convert h using 2
  -- Step 5: convert iteratedFDerivWithin to iteratedFDeriv (open sets).
  have ht_in_ball : lineCLM K ξ t ∈ Metric.ball (0 : VertexPotential K) ε := by
    rw [lineCLM_apply]; exact h_tξ_in_ball
  have h_within_eq_R :
      iteratedFDerivWithin ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (Metric.ball (0 : VertexPotential K) ε)
        (lineCLM K ξ t) =
      iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (lineCLM K ξ t) :=
    iteratedFDerivWithin_of_isOpen 3 Metric.isOpen_ball ht_in_ball
  have h_within_eq_comp :
      iteratedFDerivWithin ℝ 3
        (fun s : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            ((lineCLM K ξ) s))
        (lineCLM K ξ ⁻¹' Metric.ball (0 : VertexPotential K) ε) t =
      iteratedFDeriv ℝ 3
        (fun s : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            ((lineCLM K ξ) s)) t :=
    iteratedFDerivWithin_of_isOpen 3 h_open_pre h_t_in_pre
  -- Combine: free-space iteratedFDeriv chain-rule formula.
  have h_chain_free :
      iteratedFDeriv ℝ 3
        (fun s : ℝ =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK)
            ((lineCLM K ξ) s)) t =
      (iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (lineCLM K ξ t)).compContinuousLinearMap (fun _ : Fin 3 => lineCLM K ξ) := by
    rw [← h_within_eq_comp, h_chain_within, h_within_eq_R]
  -- Step 6: rewrite the line-restricted remainder via `lineCLM`.
  have h_eq_line :
      (fun s : ℝ =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK)
          (linePotential K ξ s)) =
      (fun s : ℝ =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK)
          ((lineCLM K ξ) s)) := by
    funext s
    rw [lineCLM_eq_linePotential]
  -- Step 7: bound `|iteratedDeriv 3 R_line t|` using the chain-rule formula.
  rw [h_eq_line]
  -- iteratedDeriv 3 f t = (iteratedFDeriv ℝ 3 f t)(fun _ => 1).
  rw [iteratedDeriv]
  rw [h_chain_free]
  -- Now: |((iteratedFDeriv 3 R (lineCLM ξ t)).compCLM (fun _ => lineCLM ξ))(fun _ => 1)|
  -- = |(iteratedFDeriv 3 R (t • ξ))(fun _ => lineCLM ξ 1)|
  -- = |(iteratedFDeriv 3 R (t • ξ))(fun _ => ξ)|
  rw [ContinuousMultilinearMap.compContinuousLinearMap_apply]
  rw [lineCLM_apply]
  -- Goal: |(iteratedFDeriv 3 R (t • ξ))(fun _ => lineCLM ξ 1)| ≤ ‖...‖ · ‖ξ‖^3
  -- Use lineCLM_one to simplify (fun _ => lineCLM K ξ 1) = (fun _ => ξ).
  have h_lcm1 : (fun _ : Fin 3 => lineCLM K ξ 1) = (fun _ : Fin 3 => ξ) := by
    funext i; exact lineCLM_one K ξ
  rw [h_lcm1]
  -- Bound by `ContinuousMultilinearMap.le_opNorm`.
  have h_op := ContinuousMultilinearMap.le_opNorm
    (iteratedFDeriv ℝ 3
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (t • ξ))
    (fun _ : Fin 3 => ξ)
  -- h_op : ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
  -- For m = const ξ on Fin 3, ∏ i, ‖ξ‖ = ‖ξ‖^3.
  have h_prod : (∏ _i : Fin 3, ‖ξ‖) = ‖ξ‖ ^ (3 : ℕ) := by
    rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin]
  -- Convert ‖_‖ to |_| for the real-valued LHS via `abs_eq_norm` on ℝ.
  have h_abs_eq : |(iteratedFDeriv ℝ 3
            (fun ξ' : VertexPotential K =>
              reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
            (t • ξ))
          (fun _ : Fin 3 => ξ)| =
        ‖(iteratedFDeriv ℝ 3
            (fun ξ' : VertexPotential K =>
              reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
            (t • ξ))
          (fun _ : Fin 3 => ξ)‖ := by
    rfl
  rw [h_abs_eq]
  calc ‖(iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (t • ξ))
        (fun _ : Fin 3 => ξ)‖
      ≤ ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (t • ξ)‖ * (∏ _i : Fin 3, ‖ξ‖) := h_op
    _ = ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (t • ξ)‖ * ‖ξ‖ ^ (3 : ℕ) := by rw [h_prod]

/-- **CLOSURE: `CanonicalRemainderIteratedFDerivLocalBoundTarget`.**

The third Fréchet derivative of the canonical remainder is locally bounded
at the flat point: by `ContDiffAt` and `ContDiffAt.continuousAt_iteratedFDeriv`,
`iteratedFDeriv ℝ 3 R` is continuous at `0`, so `‖iteratedFDeriv ℝ 3 R z‖ < ‖0‖ + 1`
for `z` close to `0`. We take `M := ‖iteratedFDeriv ℝ 3 R 0‖ + 1` and `δ` from
the continuity δ-ε statement. -/
theorem canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    CanonicalRemainderIteratedFDerivLocalBoundTarget K hK := by
  -- ContDiffAt of R at zeroPotential at order ⊤.
  have hContR : ContDiffAt ℝ (⊤ : ℕ∞)
      (fun ξ' : VertexPotential K =>
        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
      (zeroPotential K) :=
    canonicalRemainder_contDiffAt_zero_of_flatConfiguration K hK hFlat
  -- iteratedFDeriv 3 R is continuous at zeroPotential K.
  have hContAt :
      ContinuousAt
        (iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ'))
        (zeroPotential K) := by
    refine hContR.continuousAt_iteratedFDeriv (k := 3) ?_
    exact (WithTop.coe_le_coe).mpr le_top
  -- Set the bound `M := ‖iteratedFDeriv 3 R 0‖ + 1`.
  set M : ℝ := ‖iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (zeroPotential K)‖ + 1 with hM_def
  have hM_nonneg : 0 ≤ M := by
    have hpos : 0 ≤ ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
          (zeroPotential K)‖ := norm_nonneg _
    linarith
  -- Continuity at zeroPotential K with tolerance 1.
  rw [Metric.continuousAt_iff] at hContAt
  obtain ⟨δ, hδ_pos, hδ⟩ := hContAt 1 (by norm_num : (0 : ℝ) < 1)
  refine ⟨δ, M, hδ_pos, hM_nonneg, ?_⟩
  intro z hz
  -- ‖z - zeroPotential K‖ = ‖z‖ since zeroPotential K is the zero element.
  have hz_dist : dist z (zeroPotential K) < δ := by
    rw [dist_eq_norm]
    have h_zp : (zeroPotential K) = (0 : VertexPotential K) := by
      funext i; simp [zeroPotential]
    rw [h_zp]
    simpa using hz
  -- Apply continuity bound.
  have h_dist := hδ hz_dist
  -- h_dist : dist (iteratedFDeriv 3 R z) (iteratedFDeriv 3 R 0) < 1
  rw [dist_eq_norm] at h_dist
  -- ‖A - B‖ < 1 implies ‖A‖ ≤ ‖B‖ + 1 = M.
  have h_le : ‖iteratedFDeriv ℝ 3
          (fun ξ' : VertexPotential K =>
            reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z‖
        ≤ ‖iteratedFDeriv ℝ 3
            (fun ξ' : VertexPotential K =>
              reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
            (zeroPotential K)‖ + 1 := by
    have h_tri := norm_sub_norm_le
      (iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ') z)
      (iteratedFDeriv ℝ 3
        (fun ξ' : VertexPotential K =>
          reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ')
        (zeroPotential K))
    linarith
  exact h_le