hasDerivAt_costAlphaLog

formal source

  86  rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
  87    funext fun x => mul_comm x α] at h
  88
  89private lemma hasDerivAt_costAlphaLog (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
  90    HasDerivAt (CostAlphaLog α) (sinh (α * t) / α) t := by
  91  have h1 : HasDerivAt (fun s => cosh (α * s)) (sinh (α * t) * α) t :=
  92    (hasDerivAt_cosh (α * t)).comp t (hasDerivAt_alpha_mul α t)
  93  have h2 : HasDerivAt (fun s => cosh (α * s) - 1) (sinh (α * t) * α) t :=
  94    h1.sub_const 1
  95  have h_const : HasDerivAt (fun _ : ℝ => (1 / α ^ 2 : ℝ)) 0 t :=
  96    hasDerivAt_const t (1 / α ^ 2)
  97  have h3 := h_const.mul h2
  98  simp only [zero_mul, zero_add] at h3
  99  unfold CostAlphaLog
 100  convert h3 using 1
 101  field_simp
 102
 103private lemma deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
 104    deriv (CostAlphaLog α) = fun t => sinh (α * t) / α :=
 105  funext fun t => (hasDerivAt_costAlphaLog α hα t).deriv
 106
 107private lemma hasDerivAt_sinhDivAlpha (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 108    HasDerivAt (fun s => sinh (α * s) / α) (cosh (α * t)) t := by
 109  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
 110    (hasDerivAt_sinh (α * t)).comp t (hasDerivAt_alpha_mul α t)
 111  convert h1.div_const α using 1
 112  field_simp
 113
 114/-- **Calibration Invariance**: G_α''(0) = 1 for every α ≠ 0.
 115    The unit-curvature condition is independent of the rescaling parameter. -/
 116theorem costAlphaLog_unit_curvature (α : ℝ) (hα : α ≠ 0) :
 117    deriv (deriv (CostAlphaLog α)) 0 = 1 := by
 118  rw [deriv_costAlphaLog_eq α hα, (hasDerivAt_sinhDivAlpha α hα 0).deriv,
 119      mul_zero, cosh_zero]