BKLNW.bklnw_cor_8_1b

@[blueprint  "bklnw-cor-8-1b"  (title := "BKLNW Corollary 8.1b")  (statement := /-- Let $k \in \{1,\ldots,5\}$ and let $b_0$ be any entry incolumn 1 of BKLNW Table 10. Then,\begin{equation} \label{bound:mathcalB} |\theta (x) - x| \le \frac{\mathcal{B}_k(b_0) x}{(\log x)^k}  \qquad \text{for all }x \in [e^{b_0}, e^K]\end{equation}where $K = 25000$, and\begin{equation}\label{MathcalBbbprime2}\mathcal{B}_k(b_0) =\max_{\substack{b \in \mathrm{Table10}\\ b_0 \le b < K}}  B_k(b,\operatorname{next}(b)).\end{equation} -/)  (proof := /-- For $x \in [e^{b_0},e^K]$, choose the largest Table 10 entry$b$ with $b_0 \le b \le \log x$. Then$x \in [e^b,e^{\operatorname{next}(b)}]$, so \eqref{B:ExpSubinterval} applies tothis subinterval. The definition of $\mathcal{B}_k(b_0)$ as a finite maximum overthe Table 10 grid then bounds the chosen subinterval constant. -/)  (latexEnv := "sublemma")  (discussion := 1256)]theorem bklnw_cor_8_1b (k : ℕ) (b₀ : ℝ) (hk : 1 ≤ k ∧ k ≤ 5)  (hb₀ : b₀ ∈ table_10_entries) :  ∀ x ∈ Set.Icc (exp b₀) (exp K), |θ x - x| ≤ (B_8_1' k b₀) * x / (log x)^k := by  intro x hx  have hx_pos : 0 < x := (exp_pos b₀).trans_le hx.1  have hlog_lower : b₀ ≤ log x := by    simpa using log_le_log (exp_pos b₀) hx.1  have hlog_upper : log x ≤ K := by    simpa using log_le_log hx_pos hx.2  obtain ⟨b, hb_in, hb₀_le, hb_le_logx, hlogx_le_next⟩ :=    table_10_coverage b₀ (log x) hb₀ hlog_lower hlog_upper  have hb_lt_K : b < K := table_10_entry_lt_K b hb_in  have hxb : exp b ≤ x := by    simpa [exp_log hx_pos] using exp_le_exp.mpr hb_le_logx  have hxnext : x ≤ exp (table_10_next b) := by    simpa [exp_log hx_pos] using exp_le_exp.mpr hlogx_le_next  have hbk : b ≥ max 7 (2 * (k : ℝ)) := by    have hb20 : (20 : ℝ) ≤ b := table_10_entries_ge_20 b hb_in    have hk5 : (k : ℝ) ≤ 5 := by exact_mod_cast hk.2    exact max_le (by linarith) (by linarith)  have hsub :      |θ x - x| ≤ (B_8_1 k b (table_10_next b)) * x / (log x)^k :=    bklnw_cor_8_1a k b (table_10_next b) hk      (table_10_next_gt b hb_lt_K) hbk x ⟨hxb, hxnext⟩  have hB : B_8_1 k b (table_10_next b) ≤ B_8_1' k b₀ := by    let S := (table_10_entries.filter (fun b ↦ b₀ ≤ b ∧ b < K)).image      fun b ↦ B_8_1 k b (table_10_next b)    have hmem : B_8_1 k b (table_10_next b) ∈ S := mem_image_of_mem _      (mem_filter.mpr ⟨hb_in, hb₀_le, hb_lt_K⟩)    rw [B_8_1', dif_pos ⟨B_8_1 k b (table_10_next b), hmem⟩]    exact Finset.le_sup' id hmem  have hx_gt_one : 1 < x := by    have hb20 : (20 : ℝ) ≤ b₀ := table_10_entries_ge_20 b₀ hb₀    have : 1 < exp b₀ := by      simpa using exp_strictMono (by linarith : (0 : ℝ) < b₀)    exact this.trans_le hx.1  exact hsub.trans <|    div_le_div_of_nonneg_right      (mul_le_mul_of_nonneg_right hB hx_pos.le)      (pow_nonneg (log_pos hx_gt_one).le k)