lemma
proved
tactic proof
J_nonneg
show as:
view Lean formalization →
formal statement (Lean)
84lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
proof body
Tactic-mode proof.
85 unfold J
86 have hx_ne : x ≠ 0 := hx.ne'
87 have h_rewrite : (1:ℝ)/2 * (x + x⁻¹) - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
88 rw [h_rewrite]
89 apply div_nonneg (sq_nonneg _) (by linarith : 0 ≤ 2 * x)
90
91/-- J(1) = 0 (the identity has zero cost). -/