deriv_Jcost_eq

proof body

Tactic-mode proof.

  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
  60  -- h_sub gives: HasDerivAt Jcost ((1 - x⁻²) / 2) x
  61  have h_eq : (1 + -(x ^ 2)⁻¹) / 2 = (1 - x⁻¹ ^ 2) / 2 := by
  62    have h1 : (x ^ 2)⁻¹ = x⁻¹ ^ 2 := by
  63      rw [pow_two, pow_two, mul_inv_rev]
  64    rw [h1]
  65    ring
  66  rw [h_eq] at h_sub
  67  exact h_sub.deriv
  68
  69/-! ## Linearized Bond Delta -/
  70
  71/-- The linearized per-bond delta for J under log-strain L at base x. -/