BKLNW.bklnw_corollary_9_1

@[blueprint  "bklnw-corollary-9-1"  (title := "BKLNW Corollary 9.1")  (statement := /--  Let $(v,c,C) \in \{(5 \cdot 10^{10}, 0.8, 0.81), (32 \cdot 10^{12}, 0.88, 0.86), (10^{19}, 0.94, 0.94) \}$. Let $k \ge 0$ and let $b$ satisfy $\max(10^4, e^{2k}) \le e^{b} \le v$. Then \begin{equation}  \label{eqn:C-Section-Post-Corollary}  \theta(x) \ge x - \frac{\mathcal{C}_{b,k}x}{(\log x)^k} \qquad  \text{for all } x \in [e^b,v] \end{equation} where  \begin{equation}    \label{defn:mathcalCbk}    \mathcal{C}_{b,k} = b^k ( (C+1)e^{-b/2} + c_0e^{-2b/3}+ c e^{-3b/4}+ c_0 e^{-4b/5}  ),  \end{equation}and where $c_0$ is defined in Rosser-Schoenfeld.-/)  (proof := /-- We apply \eqref{eqn:C-Section-Post-Lemma} with $u=e^{\frac{b}{2}} $: \[   \theta(x) \ge x-(C +1)x^{\frac12} - cx^{\frac14}  - c_0 x^{\frac13} - c_0 x^{\frac15} \ \text{for all}\ x \in [e^b,v]. \]We now set \begin{equation}  \label{eqn:C-Section-prebound}   \mathcal{C}_{b,k} = \max_{x \in [e^b,v]  } \Big\{  (C+1)\frac{(\log x)^k}{x^\frac12} + c_0\frac{(\log x)^k}{x^\frac23} + c\frac{(\log x)^k}{x^\frac34} + c_0\frac{(\log x)^k}{x^\frac45}  \Big\}. \end{equation}We find that this equals the expression in \eqref{defn:mathcalCbk} by observing thatfor  $a \in \{ \frac12, \frac23, \frac34, \frac45 \}$, $\frac{(\log x)^k}{ x^{a}}$ is decreasing for  $x \ge e^b$ as long as $e^{b} \ge e^{k/a}$.This last inequality leads to the condition $b \ge 2k$.  -/)  (latexEnv := "corollary")  (discussion := 1262)]theorem bklnw_corollary_9_1 (k : ℕ) (v c C b : ℝ) (hvcc : (100, v, c, C) ∈ table_from_buthe) (hb : max (10000 : ℝ) (exp (2 * k)) ≤ exp b ∧ exp b ≤ v) :  ∀ x ∈ Set.Icc (exp b) v, θ x ≥ x - C_bk b c C RS_prime.c₀ k * x / (log x)^k := by  obtain ⟨hb_lb, hb_ub⟩ := hb  set u := exp (b / 2) with hu_def  obtain ⟨hbk, hu_ge_100, hb_pos, hu_lt_v, hu_ge_1, hu_sq⟩ :=    exp_half_mem_Icc_of_exp_mem k v b hb_lb hb_ub  have hψ_bound_uv : ∀ x ∈ Set.Icc u v, -c ≤ (x - ψ x) / sqrt x ∧ (x - ψ x) / sqrt x ≤ C := by    intro x hx    apply bklnw_table_from_buthe 100 v c C hvcc    exact ⟨le_trans (by exact_mod_cast hu_ge_100) hx.1, hx.2⟩  have hψ_linear : ∀ x > 0, ψ x < RS_prime.c₀ * x :=    fun x hx => RS_prime.theorem_12 hx  have hlemma9 : ∀ x ∈ Set.Icc (exp b) v,      θ x ≥ x - (C + 1) * x ^ (1 / 2 : ℝ) - RS_prime.c₀ * x ^ (1 / 3 : ℝ)              - c * x ^ (1 / 4 : ℝ) - RS_prime.c₀ * x ^ (1 / 5 : ℝ) := by    have h9 := bklnw_lemma_9 u v c C RS_prime.c₀ ⟨hu_ge_1, hu_lt_v⟩ hψ_bound_uv hψ_linear    rwa [hu_sq] at h9  intro x hx_mem  have hx_pos : (0 : ℝ) < x := (exp_pos b).trans_le hx_mem.1  have hx_log : b ≤ log x := by    have := hx_mem.1    rwa [← Real.log_exp b, Real.log_le_log_iff (exp_pos b) hx_pos]  have hterm1 := log_pow_mul_rpow_neg_le_pow_mul_exp_neg k 1 (by norm_num) b hbk x hx_pos hx_log  have hterm2 := log_pow_mul_rpow_neg_le_pow_mul_exp_neg k 2 (by norm_num) b hbk x hx_pos hx_log  have hterm3 := log_pow_mul_rpow_neg_le_pow_mul_exp_neg k 3 (by norm_num) b hbk x hx_pos hx_log  have hterm4 := log_pow_mul_rpow_neg_le_pow_mul_exp_neg k 4 (by norm_num) b hbk x hx_pos hx_log  obtain ⟨hc_nonneg, hC_nonneg⟩ := table_from_buthe_cC_nonneg v c C hvcc  have hc₀_nonneg : (0 : ℝ) ≤ RS_prime.c₀ := by norm_num [RS_prime.c₀]  have hlogk_pos : 0 < (log x) ^ k := pow_pos (by linarith) k  have hrw1 : x ^ (1 / 2 : ℝ) = x ^ (-(1 : ℝ) / (1 + 1)) * x := by    rw [show (1 / 2 : ℝ) = 1 / (1 + 1 : ℝ) by norm_num]    exact rpow_one_div_succ_eq_rpow_neg_div_mul 1 (by norm_num) x hx_pos  have hrw2 : x ^ (1 / 3 : ℝ) = x ^ (-(2 : ℝ) / (2 + 1)) * x := by    rw [show (1 / 3 : ℝ) = 1 / (2 + 1 : ℝ) by norm_num]    exact rpow_one_div_succ_eq_rpow_neg_div_mul 2 (by norm_num) x hx_pos  have hrw3 : x ^ (1 / 4 : ℝ) = x ^ (-(3 : ℝ) / (3 + 1)) * x := by    rw [show (1 / 4 : ℝ) = 1 / (3 + 1 : ℝ) by norm_num]    exact rpow_one_div_succ_eq_rpow_neg_div_mul 3 (by norm_num) x hx_pos  have hrw4 : x ^ (1 / 5 : ℝ) = x ^ (-(4 : ℝ) / (4 + 1)) * x := by    rw [show (1 / 5 : ℝ) = 1 / (4 + 1 : ℝ) by norm_num]    exact rpow_one_div_succ_eq_rpow_neg_div_mul 4 (by norm_num) x hx_pos  suffices h_sum_le : (C + 1) * x ^ (1 / 2 : ℝ) + RS_prime.c₀ * x ^ (1 / 3 : ℝ)      + c * x ^ (1 / 4 : ℝ) + RS_prime.c₀ * x ^ (1 / 5 : ℝ)      ≤ C_bk b c C RS_prime.c₀ k * x / (log x) ^ k by    linarith [hlemma9 x hx_mem]  calc (C + 1) * x ^ (1 / 2 : ℝ) + RS_prime.c₀ * x ^ (1 / 3 : ℝ)          + c * x ^ (1 / 4 : ℝ) + RS_prime.c₀ * x ^ (1 / 5 : ℝ)      _ ≤ ((C + 1) * (b ^ k * exp (-(1 : ℝ) * b / (1 + 1)))            + RS_prime.c₀ * (b ^ k * exp (-(2 : ℝ) * b / (2 + 1)))            + c * (b ^ k * exp (-(3 : ℝ) * b / (3 + 1)))            + RS_prime.c₀ * (b ^ k * exp (-(4 : ℝ) * b / (4 + 1)))) * x / (log x) ^ k := by          rw [hrw1, hrw2, hrw3, hrw4, le_div_iff₀ hlogk_pos]          nlinarith [mul_le_mul_of_nonneg_left hterm1 (by linarith : (0:ℝ) ≤ C + 1),                     mul_le_mul_of_nonneg_left hterm2 hc₀_nonneg,                     mul_le_mul_of_nonneg_left hterm3 hc_nonneg,                     mul_le_mul_of_nonneg_left hterm4 hc₀_nonneg,                     mul_nonneg (rpow_nonneg hx_pos.le (-(1 : ℝ) / (1 + 1))) hx_pos.le,                     mul_nonneg (rpow_nonneg hx_pos.le (-(2 : ℝ) / (2 + 1))) hx_pos.le,                     mul_nonneg (rpow_nonneg hx_pos.le (-(3 : ℝ) / (3 + 1))) hx_pos.le,                     mul_nonneg (rpow_nonneg hx_pos.le (-(4 : ℝ) / (4 + 1))) hx_pos.le]      _ = C_bk b c C RS_prime.c₀ k * x / (log x) ^ k := by          simp only [C_bk]; ring_nf