BKLNW.lemma_11b

@[blueprint  "bklnw-lemma-11b"  (title := "BKLNW Lemma 11b")  (statement := /-- With the hypotheses as above, we have  $$ (1 - \eps(b) - c_0(e^{-b/2} + e^{-2b/3} + e^{-4b/5})) x \leq \theta(x)$$   for all $x \geq e^b$ and $b>0$, where $c_0 = 1.03883$ is the constant from \cite[Theorem 12]{rs-prime}. -/)  (proof := /-- From Theorem \ref{costa-pereira-theorem-1a} we have $\psi(x) - \theta(x) ≤ \psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5})$.  Now apply the hypothesis on $\psi(x)$ and  Theorem \ref{rs-psi-upper}. -/)  (latexEnv := "lemma")  (discussion := 789)]theorem lemma_11b (I : Pre_inputs) {b x : ℝ} (hb : 0 < b) (hx : x ≥ exp b) :    (1 - I.ε b - RS_prime.c₀ * (exp (-b / 2) + exp (-2 * b / 3) + exp (-4 * b / 5))) * x ≤ θ x := by  have hx_pos : 0 < x := lt_of_lt_of_le (exp_pos b) hx  have hlog_x : b ≤ log x := (log_exp b).symm ▸ log_le_log (exp_pos b) hx  have hψ_half : ψ (x ^ (1 / 2 : ℝ)) < RS_prime.c₀ * x ^ (1 / 2 : ℝ) :=    RS_prime.theorem_12 <| rpow_pos_of_pos (lt_of_lt_of_le (exp_pos b) hx) _  have hψ_third : ψ (x ^ (1 / 3 : ℝ)) < RS_prime.c₀ * x ^ (1 / 3 : ℝ) :=    RS_prime.theorem_12 <| rpow_pos_of_pos hx_pos _  have hψ_fifth : ψ (x ^ (1 / 5 : ℝ)) < RS_prime.c₀ * x ^ (1 / 5 : ℝ) :=    RS_prime.theorem_12 <| rpow_pos_of_pos hx_pos _  have hψ_lower : (1 - I.ε b) * x ≤ ψ x := by grind [I.hε b hb.le x hx]  have hψ_upper : ψ x ≤ θ x + ψ (x ^ (1 / 2 : ℝ)) + ψ (x ^ (1 / 3 : ℝ)) + ψ (x ^ (1 / 5 : ℝ)) := by    have hCP : ψ x - θ x ≤ ψ (x ^ (1 / 2 : ℝ)) + ψ (x ^ (1 / 3 : ℝ)) + ψ (x ^ (1 / 5 : ℝ)) := by      simpa [one_div] using Chebyshev.psi_sub_theta_le_psi_add_psi_add_psi x    grind  have h_half : x ^ (1 / 2 : ℝ) ≤ x * exp (-b / 2) := by    rw [← log_le_log_iff (rpow_pos_of_pos hx_pos _) (mul_pos hx_pos (exp_pos _)),        log_rpow hx_pos, log_mul hx_pos.ne' (exp_pos _).ne', log_exp]    grind  have h_third : x ^ (1 / 3 : ℝ) ≤ x * exp (-2 * b / 3) := by    rw [← log_le_log_iff (rpow_pos_of_pos hx_pos _) (mul_pos hx_pos (exp_pos _)),        log_rpow hx_pos, log_mul hx_pos.ne' (exp_pos _).ne', log_exp]    grind  have h_fifth : x ^ (1 / 5 : ℝ) ≤ x * exp (-4 * b / 5) := by    rw [← log_le_log_iff (rpow_pos_of_pos hx_pos _) (mul_pos hx_pos (exp_pos _)),        log_rpow hx_pos, log_mul hx_pos.ne' (exp_pos _).ne', log_exp]    grind  have hc₀_nonneg : 0 ≤ RS_prime.c₀ := le_of_lt (by norm_num : (0 : ℝ) < 1.03883)  nlinarith