Jlog_second_deriv_at_zero

formal source

  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
  65  second_deriv_at_identity := Jcost_comp_exp_second_deriv_at_zero
  66
  67end Cost
  68end IndisputableMonolith