linJ_unit

formal source

  72noncomputable def linJ (x L : ℝ) : ℝ := ((x - x⁻¹) / 2) * L
  73
  74/-- At unit multiplier (x=1), the linear term vanishes. -/
  75lemma linJ_unit (L : ℝ) : linJ 1 L = 0 := by simp [linJ]
  76
  77/-- The key identity connecting linJ to the derivative:
  78    linJ(x, L) = J'(x) · x · L
  79
  80    Algebraic identity: (x - x⁻¹)/2 = ((1 - x⁻²)/2) · x -/
  81theorem linJ_eq_derivative_times_x (x L : ℝ) (hx : 0 < x) :
  82    linJ x L = deriv Jcost x * x * L := by
  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) -/
 105noncomputable def remJ (x L : ℝ) : ℝ :=