theorem proved term proof

`Jlog_unit_curvature`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  46theorem Jlog_unit_curvature : deriv (deriv Jlog) 0 = 1 :=

Term-mode proof.

  47  Jlog_second_deriv_at_zero
  48
  49/-- Identity: (Jcost ∘ exp) equals Jlog pointwise. -/

Lean names referenced from this declaration's body.

Jlog in IndisputableMonolith.Cost decl_use
Jlog_second_deriv_at_zero in IndisputableMonolith.Cost.Calibration decl_use
Jlog in IndisputableMonolith.Cost.FlogEL decl_use
Jlog in IndisputableMonolith.Cost.Jlog decl_use
Identity in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use