hasDerivAt_Jlog

formal source

 177  rw [Real.cosh_eq, inv_eq_one_div, Real.exp_neg]
 178  ring
 179
 180lemma hasDerivAt_Jlog (t : ℝ) : HasDerivAt Jlog (Real.sinh t) t := by
 181  have h1 : Jlog = fun t => Real.cosh t - 1 := by
 182    ext t
 183    exact Jlog_as_cosh t
 184  rw [h1]
 185  have h_cosh : HasDerivAt Real.cosh (Real.sinh t) t := Real.hasDerivAt_cosh t
 186  have h_const : HasDerivAt (fun _ => (1 : ℝ)) 0 t := hasDerivAt_const t 1
 187  have h_sub := h_cosh.sub h_const
 188  simp at h_sub
 189  exact h_sub
 190
 191@[simp] lemma hasDerivAt_Jlog_zero : HasDerivAt Jlog 0 0 := by
 192  simpa using (hasDerivAt_Jlog 0)
 193
 194@[simp] lemma deriv_Jlog_zero : deriv Jlog 0 = 0 := by
 195  classical
 196  simpa using (hasDerivAt_Jlog_zero).deriv
 197
 198theorem hasDerivAt_Jcost (x : ℝ) (hx : x ≠ 0) :
 199    HasDerivAt Jcost ((1 - x⁻¹ ^ 2) / 2) x := by
 200  unfold Jcost
 201  -- The derivative of f(x) = (x + 1/x)/2 - 1 is f'(x) = (1 - 1/x²)/2
 202  have h1 : HasDerivAt (fun y => y + y⁻¹) (1 + (-(x^2)⁻¹ : ℝ)) x := by
 203    apply HasDerivAt.add
 204    · exact hasDerivAt_id x
 205    · exact hasDerivAt_inv hx
 206  have h2 : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + (-(x^2)⁻¹)) / 2) x :=
 207    h1.div_const 2
 208  have h3 : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + (-(x^2)⁻¹)) / 2 - 0) x :=
 209    h2.sub (hasDerivAt_const x (1 : ℝ))
 210  have h_eq : (1 + (-(x^2)⁻¹)) / 2 - 0 = (1 - x⁻¹ ^ 2) / 2 := by