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

Jcost_one_plus_exact

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)

  60theorem Jcost_one_plus_exact (ε : ℝ) (hε : -1 < ε) :
  61    Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by

proof body

Tactic-mode proof.

  62  unfold Jcost
  63  have h1ε : (0 : ℝ) < 1 + ε := by linarith
  64  have h1ε_ne : (1 + ε) ≠ 0 := ne_of_gt h1ε
  65  field_simp
  66  ring
  67
  68/-- For small ε, J(1+ε) ≈ ε²/2. Specifically, the ratio approaches 1. -/

used by (5)

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