BKLNW.lem_6

@[blueprint  "bklnw-lem-6"  (title := "BKLNW Lemma 6")  (statement := /--  Suppose there exists $c_1, c_2, c_3, c_4 > 0$ such that\begin{equation}\label{bklnw_3.3}|\theta(x) - x| \leq c_1 x (\log x)^{c_2} \exp(-c_3 (\log x)^{\frac{1}{2}}) \quad \text{for all } x \geq c_4.\end{equation}Let $k > 0$ and let $b \geq \max\left(\log c_4, \log\left(\frac{4(c_2 + k)^2}{c_3^2}\right)\right)$. Then for all $x \geq e^b$ we have$$|\theta(x) - x| \leq \frac{\mathcal{A}_k(b) x}{(\log x)^k},$$where$$\mathcal{A}_k(b) = c_1 \cdot b^{c_2 + k} e^{-c_3\sqrt{b}}.$$ -/)  (proof := /-- We denote $g(x) = (\log x)^{c_2 + k} \exp(-c_3 (\log x)^{\frac{1}{2}})$. By \eqref{bklnw_3.3}, $|\theta(x) - x| < \frac{c_1 g(x) x}{(\log x)^k}$ for all $x \geq c_4$. It suffices to bound $g$: by calculus, $g(x)$ decreases when $x \geq \frac{4(c_2 + k)^2}{c_3^2}$. Therefore $|\theta(x) - x| \leq \frac{c_1 g(e^b) x}{(\log x)^k}$. Note that $c_1 g(e^b) = \mathcal{A}_k(b)$ and the condition on $b$ follows from the conditions $e^b \geq c_4$ and $e^b \geq \frac{4(c_2 + k)^2}{c_3^2}$. -/)  (latexEnv := "lemma")  (discussion := 854)]theorem lem_6 {c₁ c₂ c₃ c₄ k b x : ℝ} (hc₁ : 0 < c₁) (hc₂ : 0 < c₂) (hc₃ : 0 < c₃) (hc₄ : 0 < c₄)    (hθ : Eθ.classicalBound c₁ c₂ c₃ 1 c₄)    (hk : 0 < k)    (hb : b ≥ max (log c₄) (((4 * (c₂ + k) ^ 2) / (c₃ ^ 2))))    (hx : x ≥ exp b) :    let A := c₁ * b ^ (c₂ + k) * exp (-c₃ * sqrt b)    Eθ x ≤ A / (log x) ^ k := by      /-NOTE: the hypothesis `hb` is modified from the original source material \cite{BKLNW}, from b ≥ log ((4 * (c₂ + k) ^ 2) / (c₃ ^ 2))) to b ≥ ((4 * (c₂ + k) ^ 2) / (c₃ ^ 2))).      This corresponds to the fact that in the proof sketch above, the claim "$g(x)$ decreases when $x \geq \frac{4(c_2 + k)^2}{c_3^2}$" should be "$g(x)$ decreases when $\log x \geq \frac{4(c_2 + k)^2}{c_3^2}$."  -/      -- By `hθ`, we have $E_\theta(x) \le c_1 (\log x)^{c_2} e^{-c_3\sqrt{\log x}}$.      have h_bound : Eθ x ≤ c₁ * (Real.log x) ^ c₂ * Real.exp (-c₃ * Real.sqrt (Real.log x)) := by        convert hθ x _ using 1 <;> norm_num;        · unfold admissible_bound ; norm_num;          exact Or.inl <| Or.inl <| Real.sqrt_eq_rpow _;        · exact le_trans ( Real.log_le_iff_le_exp ( by positivity ) |>.1 ( le_trans ( le_max_left _ _ ) hb ) ) hx;      -- By `g_decreasing_interval` with $A = c_2+k$ and $C = c_3$, $g$ is decreasing on $[4(c_2+k)^2/c_3^2, \infty)$.      have h_decreasing : ∀ u v : ℝ, 4 * (c₂ + k) ^ 2 / c₃ ^ 2 ≤ u → u ≤ v → v ^ (c₂ + k) * Real.exp (-c₃ * Real.sqrt v) ≤ u ^ (c₂ + k) * Real.exp (-c₃ * Real.sqrt u) := by        -- Apply the lemma g_decreasing_interval with A = c₂ + k and C = c₃.        apply g_decreasing_interval (c₂ + k) c₃ (by linarith) (by linarith);      -- Since $b \ge 4(c_2+k)^2/c_3^2$, we have $b \le \log x$.      have h_log_x_ge_b : b ≤ Real.log x := by        exact le_trans ( by norm_num ) ( Real.log_le_log ( by positivity ) hx );      have := h_decreasing b ( Real.log x ) ( by linarith [ le_max_right ( Real.log c₄ ) ( 4 * ( c₂ + k ) ^ 2 / c₃ ^ 2 ) ] ) h_log_x_ge_b; simp_all +decide only [ge_iff_le, sup_le_iff, neg_mul,        Real.rpow_add            (show 0 < Real.log x from              lt_of_lt_of_le                (by                  linarith [le_max_left (Real.log c₄) (4 * (c₂ + k) ^ 2 / c₃ ^ 2),                    le_max_right (Real.log c₄) (4 * (c₂ + k) ^ 2 / c₃ ^ 2),                    show 0 < 4 * (c₂ + k) ^ 2 / c₃ ^ 2 by positivity])                h_log_x_ge_b)]      rw [ le_div_iff₀ ( Real.rpow_pos_of_pos ( show 0 < Real.log x from lt_of_lt_of_le ( by linarith [ show 0 < 4 * ( c₂ + k ) ^ 2 / c₃ ^ 2 by positivity ] ) h_log_x_ge_b ) _ ) ] ; nlinarith [ Real.rpow_pos_of_pos ( show 0 < Real.log x from lt_of_lt_of_le ( by linarith [ show 0 < 4 * ( c₂ + k ) ^ 2 / c₃ ^ 2 by positivity ] ) h_log_x_ge_b ) k ] ;