BKLNW.bklnw_lemma_8

@[blueprint  "bklnw-lemma-8"  (title := "Lemma 8")  (statement := /--  Let $k=1,\ldots,5$. Assume there exist a positive integer $n$, real numbers $a_{\ell} \ge 0$ for every $\ell \in \{1, 2, \ldots, n \}$. and $x_0 > 0$ such that \begin{equation}  \label{psithetadiff}  \psi (x) - \theta (x) \le \sum_{\ell=1}^n a_{\ell} x^{\frac{1}{\ell+1}} \qquad \text{ for all } x \ge x_0. \end{equation} Let $b' > b \ge 2k$, $x_0 \le e^b$, and assume that there exists $\varepsilon(b)>0$ such that  \begin{equation}  \label{psixdiff}  |\psi (x) - x| \le \varepsilon(b)x \qquad \text{for all }x \ge e^{b}. \end{equation}Then we have \begin{equation}  \label{thetakBbd}   |\theta(x)-x| \le   \frac{B_k x}{(\log x)^k} \qquad  \text{for all }x \in [e^{b}, e^{b'}] \end{equation}where\begin{equation}  \label{defn:B}  B_k = B_k(b,b') =  \max_{x \in [e^b, e^{b'}]}   \Big(  \sum_{\ell=1}^n a_{\ell} (\log x)^k x^{-\frac{\ell}{\ell+1}} +  \varepsilon(b) (\log x)^k  \Big).\end{equation}   -/)  (proof := /--  By the triangle inequality and the non-negativity of $\psi(x)-\theta(x)$, we have \begin{align*}  |\theta (x) - x|  & \le  \psi (x) - \theta (x) + |\psi(x) - x|. \end{align*} Bounding these terms by (\ref{psithetadiff}) and (\ref{psixdiff}), we have for $x \ge e^b$, \begin{align*}  |\theta(x) - x| &\le   \frac{x}{(\log x)^k} \Big(  \sum_{\ell=1}^n a_{\ell} (\log x)^k x^{-\frac{\ell}{\ell+1}} +  \varepsilon(b) (\log x)^k  \Big). \end{align*}This immediately implies \eqref{thetakBbd} holds with \eqref{defn:B}.-/)  (latexEnv := "sublemma")  (discussion := 1252)]theorem bklnw_lemma_8 (k n : ℕ) (a : ℕ → ℝ) (ε : ℝ → ℝ) (b b' x₀ : ℝ)  (hk : 1 ≤ k ∧ k ≤ 5)  (hbk : b ≥ 2 * k) (hbx₀ : x₀ ≤ exp b)  (hx : ∀ x ≥ x₀, ψ x - θ x ≤ ∑ ℓ ∈ Finset.Icc 1 n, a ℓ * x ^ (1 / (ℓ + 1 : ℝ)))  (hε : ∀ x ≥ exp b, abs (ψ x - x) ≤ ε b * x)  :  ∀ x ∈ Set.Icc (exp b) (exp b'), abs (θ x - x) ≤ B k n a ε b b' * x / (log x)^k := by  intro x hx_mem  have hx_ge_exp_b : x ≥ exp b := hx_mem.1  have hx_le_exp_b' : x ≤ exp b' := hx_mem.2  have hx_ge_x0 : x ≥ x₀ := hbx₀.trans hx_ge_exp_b  have hx_pos : 0 < x := lt_of_lt_of_le (exp_pos b) hx_ge_exp_b  have h_log_x_pos : 0 < log x := by    have hk_real : (k : ℝ) ≥ 1 := by exact_mod_cast hk.1    have h_log_ge : b ≤ log x := (log_exp b).symm ▸ log_le_log (exp_pos b) hx_ge_exp_b    linarith [h_log_ge, hbk, hk_real]  calc    abs (θ x - x) ≤ abs (θ x - ψ x) + abs (ψ x - x) := abs_sub_le (θ x) (ψ x) x    _ = (ψ x - θ x) + abs (ψ x - x) := by      rw [abs_sub_comm, abs_of_nonneg (sub_nonneg.mpr (theta_le_psi x))]    _ ≤ (∑ ℓ ∈ Finset.Icc 1 n, a ℓ * x ^ (1 / (ℓ + 1 : ℝ))) + ε b * x :=      add_le_add (hx x hx_ge_x0) (hε x hx_ge_exp_b)    _ = ((∑ ℓ ∈ Finset.Icc 1 n, a ℓ * (log x)^k * x ^ (-(ℓ:ℝ) / (ℓ + 1))) + ε b * (log x) ^ k) * (x / (log x)^k) := by      rw [add_mul, Finset.sum_mul]      congr 1      · exact Finset.sum_congr rfl fun ℓ _ => bklnw_lemma_8_term_eq k ℓ x (a ℓ) hx_pos h_log_x_pos      · field_simp    _ ≤ B k n a ε b b' * (x / (log x)^k) :=      mul_le_mul_of_nonneg_right (bklnw_lemma_8_bound_le_B k n a ε b b' x hx_mem) (by positivity)    _ = B k n a ε b b' * x / (log x)^k := by      field_simp