theorem
proved
term proof
unique_cost_on_pos
show as:
view Lean formalization →
formal statement (Lean)
194theorem unique_cost_on_pos (F : ℝ → ℝ) (hF : UniqueCostAxioms F) :
195 ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
proof body
Term-mode proof.
196 T5_uniqueness_complete F hF.symmetric hF.unit hF.convex hF.calibrated hF.continuousOn_pos hF.coshAdd
197 hF.dAlembert_smooth hF.dAlembert_toODE hF.ode_cont hF.ode_diff hF.ode_bootstrap
198
199/-! ## RegularityCert for Jcost -/
200
201/-- Jcost satisfies the RegularityCert requirements: continuous on (0,∞),
202 strictly convex on (0,∞), and calibrated (second log-derivative = 1 at 0). -/