J_log_pos

formal source

  81    simp [h, J_log]
  82
  83/-- J_log is strictly positive for t ≠ 0. -/
  84theorem J_log_pos {t : ℝ} (ht : t ≠ 0) : J_log t > 0 := by
  85  have hne : J_log t ≠ 0 := fun h => ht (J_log_eq_zero_iff.mp h)
  86  have hge : J_log t ≥ 0 := J_log_nonneg t
  87  exact lt_of_le_of_ne hge (Ne.symm hne)
  88
  89/-- J_log is symmetric: J_log(-t) = J_log(t). -/
  90theorem J_log_symmetric (t : ℝ) : J_log (-t) = J_log t := by
  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