deriv2_Jlog

formal source

  31  exact (hasDerivAt_Jlog_new t).deriv
  32
  33/-- Second derivative of Jlog is cosh -/
  34lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by
  35  have h1 : deriv Jlog = sinh := by
  36    funext s; exact deriv_Jlog s
  37  rw [h1]
  38  exact (hasDerivAt_sinh t).deriv
  39
  40/-- The calibration theorem: second derivative at zero equals 1 -/
  41theorem Jlog_second_deriv_at_zero : deriv (deriv Jlog) 0 = 1 := by
  42  rw [deriv2_Jlog]
  43  exact cosh_zero
  44
  45/-- Alternative formulation: Jlog has unit curvature at the identity -/
  46theorem Jlog_unit_curvature : deriv (deriv Jlog) 0 = 1 :=
  47  Jlog_second_deriv_at_zero
  48
  49/-- Identity: (Jcost ∘ exp) equals Jlog pointwise. -/
  50lemma Jcost_comp_exp_eq_Jlog : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl
  51
  52/-- Calibration for Jcost in log-coordinates: second derivative at zero is 1. -/
  53theorem Jcost_comp_exp_second_deriv_at_zero :
  54    deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1 := by
  55  -- Jcost ∘ exp = Jlog by definition
  56  have h : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl
  57  rw [h]
  58  exact Jlog_second_deriv_at_zero
  59
  60/-- Package the calibration axiom -/
  61class UnitCurvature (F : ℝ → ℝ) : Prop where
  62  second_deriv_at_identity : deriv (deriv (F ∘ exp)) 0 = 1
  63
  64instance : UnitCurvature Jcost where