pith. machine review for the scientific record. sign in
theorem proved tactic proof

unique_cost_on_pos_from_rcl

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 167theorem unique_cost_on_pos_from_rcl (F : ℝ → ℝ)
 168    (hRecip : FunctionalEquation.IsReciprocalCost F)
 169    (hNorm : FunctionalEquation.IsNormalized F)
 170    (hComp : FunctionalEquation.SatisfiesCompositionLaw F)
 171    (hCalib : FunctionalEquation.IsCalibrated F)
 172    (hCont : ContinuousOn F (Ioi 0))
 173    (h_smooth : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
 174    (h_ode : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
 175    (h_cont : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
 176    (h_diff : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
 177    (h_boot : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
 178    ∀ {x : ℝ}, 0 < x → F x = Jcost x := by

proof body

Tactic-mode proof.

 179  intro x hx
 180  exact FunctionalEquation.washburn_uniqueness F
 181    hRecip hNorm hComp hCalib hCont h_smooth h_ode h_cont h_diff h_boot x hx
 182
 183/- Jcost satisfies the non-axiomatic hypothesis bundle (unused here)
 184 def Jcost_satisfies_axioms : UniqueCostAxioms Jcost where
 185  symmetric := fun hx => Jcost_symm hx
 186  unit := Jcost_unit0
 187  convex := Jcost_strictConvexOn_pos
 188  calibrated := by
 189    simpa using IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 190  continuousOn_pos := Jcost_continuous_pos
 191  coshAdd := FunctionalEquation.Jcost_cosh_add_identity -/
 192
 193/-- Main uniqueness statement on ℝ₊: any admissible cost equals Jcost on (0,∞). -/

depends on (28)

Lean names referenced from this declaration's body.