BKLNW.prop_4_a

@[blueprint  "bklnw-prop-4-a"  (title := "BKLNW Proposition 4, part a")  (statement := /--  If $7 \leq b \leq 2\log x_1$, then we have\begin{equation}\theta(x^{1/2}) \leq (1 + \varepsilon(\log x_1))x^{1/2} \quad \text{for } x \geq e^b.\end{equation} -/)  (proof := /--Note that in the paper, the inequality in Proposition 4 is strict, but theargument can only show nonstrict inequalities.If $e^b \leq x \leq x_1^2$, then $x^{1/2} \leq x_1$, and thus\[\theta(x^{1/2}) < x^{1/2} \quad \text{for } e^b \leq x \leq x_1^2.\]On the other hand, if $x^{1/2} > x_1 = e^{\log x_1}$, then we have by (2.7)\[\theta(x^{1/2}) \leq \psi(x^{1/2}) \leq (1 + \varepsilon(\log x_1))x^{1/2},\]since $\log x_1 \geq 7$. The last two inequalities for $\theta(x^{1/2})$ combine to establish (2.8). -/)  (latexEnv := "proposition")  (discussion := 641)]theorem prop_4_a (I : Inputs) {b x : ℝ} (hx : exp b ≤ x) :    θ (x ^ (1 / 2 : ℝ)) ≤ (1 + I.ε (log I.x₁)) * x ^ (1 / 2 : ℝ) := by  have ha : 1 < I.x₁ := by linarith [I.hx₁, (one_lt_exp_iff.2 (by linarith) : 1 < exp 7)]  have hb : 0 < log I.x₁ := log_pos (by linarith)  by_cases! hp : x ^ (1 / 2 : ℝ) ≤ I.x₁  · have hq : 0 < x ^ (1 / 2 : ℝ) := by      suffices 0 < x from rpow_pos_of_pos this _      exact (exp_pos b).trans_le hx    refine (I.hx₁' (x ^ (1 / 2 : ℝ)) ⟨hq, hp⟩).le.trans ?_    nth_rw 1 [← one_mul (x ^ (1 / 2 : ℝ))]    gcongr    linarith [I.epsilon_nonneg hb.le]  · calc    _ ≤ ψ (x ^ (1 / 2 : ℝ)) := theta_le_psi _    _ ≤ (1 + I.ε (log I.x₁)) * x ^ (1 / 2 : ℝ) := by      have := (le_abs_self (ψ (x ^ (1 / 2 : ℝ)) - x ^ (1 / 2 : ℝ))).trans <|        I.hε (log I.x₁) hb.le (x ^ (1 / 2 : ℝ)) (exp_log (by linarith : 0 < I.x₁) ▸ hp).le      linarith