klQuadratic_zero

formal source

  39  Jlog_as_cosh u
  40
  41/-- The KL quadratic has zero value at equilibrium. -/
  42@[simp] theorem klQuadratic_zero : klQuadratic 0 = 0 := by
  43  simp [klQuadratic]
  44
  45/-- The KL quadratic has zero first derivative at equilibrium. -/
  46theorem hasDerivAt_klQuadratic (u : ℝ) :
  47    HasDerivAt klQuadratic u u := by
  48  unfold klQuadratic
  49  have hsq : HasDerivAt (fun v : ℝ => v ^ 2) (2 * u) u := by
  50    simpa using (hasDerivAt_pow 2 u)
  51  have h := hsq.div_const 2
  52  convert h using 1
  53  ring
  54
  55@[simp] theorem deriv_klQuadratic_zero : deriv klQuadratic 0 = 0 := by
  56  simpa using (hasDerivAt_klQuadratic 0).deriv
  57
  58/-- The second derivative of the KL quadratic at equilibrium is `1`. -/
  59theorem hasDerivAt_deriv_klQuadratic_zero :
  60    HasDerivAt (deriv klQuadratic) 1 0 := by
  61  have h_eq : deriv klQuadratic = fun u : ℝ => u := by
  62    funext u
  63    exact (hasDerivAt_klQuadratic u).deriv
  64  rw [h_eq]
  65  simpa using (hasDerivAt_id 0)
  66
  67/-- The second derivative of log-coordinate J-cost at equilibrium is `1`. -/
  68theorem hasDerivAt_deriv_Jlog_zero :
  69    HasDerivAt (deriv Jlog) 1 0 := by
  70  have h_eq : deriv Jlog = Real.sinh := by
  71    funext u
  72    exact (hasDerivAt_Jlog u).deriv