jcost_deriv

formal source

  80/-! ## II. Gradient of J-Cost (Computability of First-Order Optimization) -/
  81
  82/-- The derivative of J-cost: J'(x) = (1 - 1/x²)/2 = (x² - 1)/(2x²). -/
  83noncomputable def jcost_deriv (x : ℝ) : ℝ := (1 - (x⁻¹)^2) / 2
  84
  85/-- **THEOREM IC-005.6**: J'(1) = 0 — the gradient vanishes at the ground state.
  86    This confirms x = 1 is the unique critical point (and global minimum). -/
  87theorem jcost_deriv_zero_at_one : jcost_deriv 1 = 0 := by
  88  unfold jcost_deriv; simp
  89
  90/-- **THEOREM IC-005.7**: J'(x) > 0 for x > 1.
  91    The gradient points upward away from the minimum for x > 1. -/
  92theorem jcost_deriv_pos_of_gt_one (x : ℝ) (hx : x > 1) :
  93    jcost_deriv x > 0 := by
  94  unfold jcost_deriv
  95  apply div_pos _ (by norm_num)
  96  have hxpos : (0 : ℝ) < x := by linarith
  97  have hxinv_lt1 : x⁻¹ < 1 := by
  98    rw [inv_eq_one_div, div_lt_one (by linarith : (0:ℝ) < x)]; linarith
  99  have hxinv_pos : (0 : ℝ) < x⁻¹ := inv_pos.mpr hxpos
 100  have : 1 - (x⁻¹)^2 > 0 := by
 101    have h4 : (1 - x⁻¹) * (1 + x⁻¹) = 1 - (x⁻¹)^2 := by ring
 102    rw [← h4]
 103    exact mul_pos (by linarith) (by linarith)
 104  linarith
 105
 106/-- **THEOREM IC-005.8**: J'(x) < 0 for 0 < x < 1.
 107    The gradient points downward, pushing toward the minimum for x < 1. -/
 108theorem jcost_deriv_neg_of_lt_one (x : ℝ) (hx : x > 0) (hlt : x < 1) :
 109    jcost_deriv x < 0 := by
 110  unfold jcost_deriv
 111  apply div_neg_of_neg_of_pos _ (by norm_num)
 112  have : (x⁻¹)^2 > 1 := by
 113    apply one_lt_pow₀ _ (by norm_num)