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

spatial_cost_positive

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)

  87theorem spatial_cost_positive (ε : ℝ) (hε : -1 < ε) (hε_ne : ε ≠ 0) :
  88    0 < Jcost (1 + ε) := by

proof body

Term-mode proof.

  89  rw [Jcost_near_identity ε hε]
  90  exact div_pos (sq_pos_of_ne_zero hε_ne) (mul_pos (by norm_num : (0:ℝ) < 2) (by linarith))
  91
  92/-- **The spatial metric coefficient** at the identity is 1/2,
  93    giving J''(1) = 2 · (1/2) = 1. -/

depends on (7)

Lean names referenced from this declaration's body.