Eθ.hasPrimeInInterval

@[blueprint  "etheta-pi"  (title := "Upper bound on Etheta implies prime in short interval")  (statement := /--  There is a prime in $(x, x+h]$ if $x E_\theta(x) + (x+h) E_\theta(x+h) < h$. -/)  (proof := /-- Lower bound $\theta(x+h) - \theta(x)$ using  $\theta(x+h) \geq x+h (1 - E_\theta(x+h))$ and $\theta(x) \leq x (1 + E_\theta(x))$  and apply Lemma \ref{theta-inc}. -/)  (latexEnv := "lemma")  (discussion := 906)]lemma Eθ.hasPrimeInInterval (x h : ℝ) (hx : 0 < x) (hh : 0 < h) :    x * Eθ x + (x + h) * Eθ (x + h) < h → HasPrimeInInterval x h := by  intro hE  have hxh : 0 < x + h := by linarith  have hx_bound : θ x ≤ x + x * Eθ x := by    have hx_abs : x * Eθ x = |θ x - x| := by      unfold Eθ      field_simp [hx.ne']    have habs : |θ x - x| ≤ x * Eθ x := by      simp [hx_abs]    linarith [abs_sub_le_iff.mp habs |>.1]  have hxh_bound : (x + h) - (x + h) * Eθ (x + h) ≤ θ (x + h) := by    have hxh_abs : (x + h) * Eθ (x + h) = |θ (x + h) - (x + h)| := by      unfold Eθ      field_simp [hxh.ne']    have habs : |θ (x + h) - (x + h)| ≤ (x + h) * Eθ (x + h) := by      simp [hxh_abs]    linarith [abs_sub_le_iff.mp habs |>.2]  have htheta : θ (x + h) > θ x := by    linarith [hx_bound, hxh_bound, hE]  exact (HasPrimeInInterval.iff_theta_ge x h).2 htheta