fix: missing positivity condition in erdos_1003.variants.eps87 (#1154)

Statement is false if `x` is negative

Author: smmercuri

FormalConjectures/ErdosProblems/1003.lean

@@ -52,7 +52,7 @@ is at most $$\frac{x}{\exp(c(\log x)^{1/3})}$$ for some constant $c > 0$.
 [EPS87] Erd\H os, Paul and Pomerance, Carl and S\'ark\"ozy, Andr\'as, _On locally repeated values of certain arithmetic functions_. {III}. Proc. Amer. Math. Soc. (1987), 1--7.
 -/
 @[category research solved, AMS 11]
-theorem erdos_1003.variants.eps87 (x : ℝ) : ∃ c > 0,
+theorem erdos_1003.variants.eps87 {x : ℝ} (hx : 0 < x) : ∃ c > 0,
     {(n : ℕ) | (n ≤ x) ∧ φ n = φ (n + 1)}.ncard ≤
       x / Real.exp (c * (x.log) ^ (1 / 3)) := by
   sorry