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

jcost_squared_form

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)

  59theorem jcost_squared_form (x : ℝ) (hx : x > 0) :
  60    Jcost x = (x - 1)^2 / (2 * x) :=

proof body

Term-mode proof.

  61  Cost.Jcost_eq_sq hx.ne'
  62
  63/-- **THEOREM IC-005.4**: J-cost is strictly positive away from x = 1.
  64    The "violation" from the ground state is proportional to (x-1)²/(2x) > 0. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.