J_log_eq_J_exp

formal source

  91  simp only [J_log, Real.cosh_neg]
  92
  93/-- Connection to original J: J(eᵗ) = J_log(t) for t corresponding to positive x. -/
  94theorem J_log_eq_J_exp (t : ℝ) : J_log t = defect (Real.exp t) := by
  95  simp only [J_log, defect, J, Real.cosh_eq]
  96  rw [Real.exp_neg]
  97
  98/-! ## Curvature at the Minimum -/
  99
 100/-- The second derivative of J_log at t = 0 is 1.
 101    This sets the "stiffness" of the cost bowl and determines
 102    the minimum step cost for discrete configurations. -/
 103theorem J_log_second_deriv_at_zero : deriv (deriv J_log) 0 = 1 := by
 104  -- J_log(t) = cosh(t) - 1
 105  -- J_log'(t) = sinh(t)
 106  -- J_log''(t) = cosh(t)
 107  -- J_log''(0) = cosh(0) = 1
 108  have h1 : deriv J_log = Real.sinh := by
 109    ext t
 110    unfold J_log
 111    rw [deriv_sub_const, Real.deriv_cosh]
 112  rw [h1, Real.deriv_sinh]
 113  exact Real.cosh_zero
 114
 115/-- **HYPOTHESIS**: Quadratic approximation of cosh(x) has a tight fourth-order bound.
 116    For |x| < 1, the Taylor remainder satisfies |cosh x - 1 - x²/2| ≤ x⁴/20.
 117    Proof follows from bounding the series Σ x^(2n)/(2n)! by its first term and a geometric tail. -/
 118theorem cosh_quadratic_bound (x : ℝ) (hx : |x| < 1) : |Real.cosh x - 1 - x^2 / 2| ≤ x^4 / 20 := by
 119  -- Power series: `cosh x = ∑' n, x^(2n)/(2n)!`.  Peel off `n=0,1` and bound the tail by a
 120  -- geometric series using the ratio test with the crude uniform bound `((2n+2)(2n+1)) ≥ 30`.
 121  let a : ℕ → ℝ := fun n => x ^ (2 * n) / (↑(2 * n).factorial)
 122  have hcosh : HasSum a (Real.cosh x) := by
 123    simpa [a] using Real.hasSum_cosh x
 124  have ha : Summable a := hcosh.summable