theorem
proved
tactic proof
global_minimum_unique
show as:
view Lean formalization →
formal statement (Lean)
52theorem global_minimum_unique (x : ℝ) (hx : 0 < x) :
53 Jcost x = 0 ↔ x = 1 := by
proof body
Tactic-mode proof.
54 constructor
55 · intro h
56 have hx0 : x ≠ 0 := ne_of_gt hx
57 rw [Jcost_eq_sq hx0] at h
58 have h_denom : 0 < 2 * x := by positivity
59 have h_sq : (x - 1) ^ 2 = 0 := by
60 by_contra hne
61 have hpos : 0 < (x - 1) ^ 2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hne)
62 have : 0 < (x - 1) ^ 2 / (2 * x) := div_pos hpos h_denom
63 linarith
64 have : x - 1 = 0 := by
65 rcases sq_eq_zero_iff.mp h_sq with h
66 exact h
67 linarith
68 · intro h; rw [h]; exact Jcost_unit0
69
70/-- Fixed points of R-hat are J-cost local minima. -/