deriv_Jlog_zero

formal source

 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
 211    have : (x^2)⁻¹ = x⁻¹ ^ 2 := by rw [inv_pow]
 212    linarith [this]
 213  rw [← h_eq]
 214  exact h3
 215
 216theorem deriv_Jcost_one : deriv Jcost 1 = 0 := by
 217  have h : HasDerivAt Jcost ((1 - 1⁻¹ ^ 2) / 2) 1 := hasDerivAt_Jcost 1 (by norm_num)
 218  simp at h
 219  exact h.deriv
 220
 221/-!
 222## Strict Convexity of Jcost
 223
 224The theorem `Jcost_strictConvexOn_pos : StrictConvexOn ℝ (Set.Ioi 0) Jcost`