differentiableAt_Jcost

formal source

  26/-! ## J-cost Basic Properties -/
  27
  28/-- J(x) = (x + x⁻¹)/2 - 1 is differentiable for x > 0. -/
  29lemma differentiableAt_Jcost (x : ℝ) (hx : 0 < x) : DifferentiableAt ℝ Jcost x := by
  30  have hxne : x ≠ 0 := ne_of_gt hx
  31  unfold Jcost
  32  apply DifferentiableAt.sub
  33  · apply DifferentiableAt.div_const
  34    apply DifferentiableAt.add differentiableAt_id
  35    exact differentiableAt_inv hxne
  36  · exact differentiableAt_const 1
  37
  38/-- The derivative of J at x equals (1 - x⁻²)/2.
  39
  40    Proof: J(x) = (x + x⁻¹)/2 - 1
  41    J'(x) = d/dx[(x + x⁻¹)/2 - 1] = (1 + (-x⁻²))/2 = (1 - x⁻²)/2
  42
  43    **Technical note**: This is standard calculus, using:
  44    - d/dx[x] = 1
  45    - d/dx[x⁻¹] = -x⁻² -/
  46lemma deriv_Jcost_eq (x : ℝ) (hx : 0 < x) :
  47    deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
  48  have hxne : x ≠ 0 := ne_of_gt hx
  49  -- J(x) = (x + x⁻¹)/2 - 1
  50  -- J'(x) = (1 + d/dx[x⁻¹])/2 = (1 - x⁻²)/2
  51  -- Use HasDerivAt to compute the derivative
  52  have h_inv : HasDerivAt (·⁻¹) (-(x ^ 2)⁻¹) x := hasDerivAt_inv hxne
  53  have h_id : HasDerivAt id 1 x := hasDerivAt_id x
  54  have h_add : HasDerivAt (fun y => y + y⁻¹) (1 + -(x ^ 2)⁻¹) x :=
  55    h_id.add h_inv
  56  have h_div : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + -(x ^ 2)⁻¹) / 2) x :=
  57    h_add.div_const 2
  58  have h_sub : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + -(x ^ 2)⁻¹) / 2) x :=
  59    h_div.sub_const 1