J_log_second_deriv_at_zero

formal source

 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
 125  have hsplit : Real.cosh x = (∑ i ∈ Finset.range 2, a i) + ∑' n, a (n + 2) := by
 126    calc
 127      Real.cosh x = ∑' n, a n := by
 128        simpa using hcosh.tsum_eq.symm
 129      _ = (∑ i ∈ Finset.range 2, a i) + ∑' n, a (n + 2) := by
 130        -- `Summable.sum_add_tsum_nat_add` gives `sum + tail = tsum`; we use its symmetric form.
 131        simpa using (Summable.sum_add_tsum_nat_add 2 ha).symm
 132  have hsum2 : (∑ i ∈ Finset.range 2, a i) = 1 + x^2 / 2 := by
 133    simp only [Finset.sum_range_succ, Finset.sum_range_zero, a]