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

Jcost_one_plus_eps

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)

  72theorem Jcost_one_plus_eps {eps : ℝ} (heps : 0 ≤ eps) :
  73    Jcost (1 + eps) = eps ^ 2 / (2 * (1 + eps)) := by

proof body

Tactic-mode proof.

  74  unfold Jcost
  75  have hne : (1 : ℝ) + eps ≠ 0 := by linarith
  76  field_simp [hne]; ring
  77
  78/-- J(1+eps) <= eps^2/2 for eps >= 0.
  79
  80Proof: eps^2/(2*(1+eps)) <= eps^2/2 because 1+eps >= 1 and the numerator
  81is nonneg. -/

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.