lemma
proved
tactic proof
Jcost_deriv
show as:
view Lean formalization →
formal statement (Lean)
223lemma Jcost_deriv (x : ℝ) (hx : x ≠ 0) :
224 deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
proof body
Tactic-mode proof.
225 unfold Jcost
226 have hdiff : DifferentiableAt ℝ (fun y => (y + y⁻¹) / 2 - 1) x := by
227 apply DifferentiableAt.sub
228 · apply DifferentiableAt.div_const
229 apply DifferentiableAt.add differentiableAt_id (differentiableAt_inv hx)
230 · exact differentiableAt_const 1
231 have h : deriv (fun y => (y + y⁻¹) / 2 - 1) x = (1 - x⁻¹ ^ 2) / 2 := by
232 have h1 : HasDerivAt (fun y => y) 1 x := hasDerivAt_id x
233 have h2 : HasDerivAt (fun y => y⁻¹) (-(x^2)⁻¹) x := hasDerivAt_inv hx
234 have h3 : HasDerivAt (fun y => y + y⁻¹) (1 + -(x^2)⁻¹) x := h1.add h2
235 have h4 : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + -(x^2)⁻¹) / 2) x := h3.div_const 2
236 have h5 : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + -(x^2)⁻¹) / 2) x := h4.sub_const 1
237 rw [h5.deriv]
238 field_simp [hx]
239 ring
240 exact h
241
242/-- J-cost is strictly increasing on (1, ∞) -/