linJ_eq_derivative_times_x

proof body

Tactic-mode proof.

  83  have hxne : x ≠ 0 := ne_of_gt hx
  84  rw [deriv_Jcost_eq x hx]
  85  unfold linJ
  86  -- Key algebraic step: (1 - x⁻²) * x = x - x⁻¹
  87  have h_key : (1 - x⁻¹ ^ 2) * x = x - x⁻¹ := by
  88    have h1 : x⁻¹ ^ 2 * x = x⁻¹ := by
  89      rw [pow_two]
  90      calc x⁻¹ * x⁻¹ * x = x⁻¹ * (x⁻¹ * x) := by ring
  91        _ = x⁻¹ * 1 := by rw [inv_mul_cancel₀ hxne]
  92        _ = x⁻¹ := by ring
  93    calc (1 - x⁻¹ ^ 2) * x
  94        = x - x⁻¹ ^ 2 * x := by ring
  95      _ = x - x⁻¹ := by rw [h1]
  96  calc ((x - x⁻¹) / 2) * L
  97      = (x - x⁻¹) / 2 * L := by ring
  98    _ = ((1 - x⁻¹ ^ 2) * x) / 2 * L := by rw [h_key]
  99    _ = (1 - x⁻¹ ^ 2) / 2 * x * L := by ring
 100
 101/-! ## Remainder Bound -/
 102
 103/-- The remainder term after linearization:
 104    rem(x, L) = J(x·e^L) - J(x) - linJ(x, L) -/