BKLNW.cor_3_1

@[blueprint  "bklnw-cor-3-1"  (title := "BKLNW Corollary 3.1")  (statement := /--  Let $b \geq 7$. Assume $x \geq e^b$. Then we have\[\psi(x) - \theta(x) - \theta(x^{1/2}) \leq \eta x^{1/3},\]where\begin{equation}\eta = (1 + \alpha) \max\left( f(e^b), f(2^{\lfloor \frac{b}{\log 2} \rfloor + 1}) \right)\end{equation} -/)  (proof := /-- We apply Proposition \ref{bklnw-prop-3} with $x_0 = e^b$ where we observe that $x_0 = e^b \geq e^7 > 2^9$. -/)  (latexEnv := "corollary")  (discussion := 640)]theorem cor_3_1 (I : Inputs) {b x : ℝ} (hb : b ≥ 7) (hx : x ≥ exp b) :    ψ x - θ x - θ (x^(1/2:ℝ)) ≤      (1 + I.α) * max (f (exp b)) (f (2^(⌊b / (log 2)⌋ + 1))) * x^(1/3:ℝ) := by  let x₀ := exp b  have : x₀ ≥ 2 ^ 9 := by    refine le_trans ?_ (exp_le_exp_of_le hb)    rw [← exp_one_rpow]    refine le_trans ?_ (rpow_le_rpow (by norm_num) exp_one_gt_d9.le (by norm_num))    norm_num  calc    _ = ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ ((1 : ℝ) / n)) - θ (x ^ (1/2 : ℝ)) := by      rw [Chebyshev.psi_eq_theta_add_sum_theta (by linarith)]; ring    _ = ∑ n ∈ Icc 3 ⌊log x / log 2⌋₊, θ (x ^ ((1 : ℝ) / n)) := by      have : ⌊log x / log 2⌋₊ ≥ 2 := calc          _ ≥ ⌊b / log 2⌋₊ := by gcongr; rw [← log_exp b]; exact log_le_log (by linarith) hx          _ ≥ 2 := by apply Nat.le_floor; field_simp; norm_num; linarith [log_two_lt_d9, hb]      rw [← add_sum_Ioc_eq_sum_Icc this, ← Icc_add_one_left_eq_Ioc]; ring_nf    _ = ∑ n ∈ Icc 3 ⌊log x / log 2⌋₊, θ (x ^ ((1 : ℝ) / n)) := by      refine sum_bij (fun n _ ↦ n) ?_ ?_ ?_ ?_      · intro n hn; simp only [mem_Icc] at hn ⊢        exact ⟨by exact_mod_cast hn.1, by exact_mod_cast hn.2⟩      · intro _ _ _ _ h; exact h      · intro n hn; simp only [mem_Icc] at hn ⊢        refine ⟨n, ?_, rfl⟩        exact ⟨by exact_mod_cast hn.1, by exact_mod_cast hn.2⟩      · intro _ _; simp only [one_div]    _ ≤ (1 + I.α) * max (f x₀) (f (2 ^ (⌊log x₀ / log 2⌋₊ + 1))) * x ^ (1/3 : ℝ) := by      exact prop_3 I this hx    _ ≤ (1 + I.α) * max (f (exp b)) (f (2 ^ (⌊b / log 2⌋ + 1))) * x ^ (1/3 : ℝ) := by      gcongr      · exact rpow_nonneg (le_trans (by linarith) hx) _      · have := I.hα 1        grind [show 0 ≤ θ 1 from sum_nonneg fun _ _ ↦ log_nonneg <| Nat.one_le_cast.2 <|          Nat.Prime.pos <| by grind only [= mem_filter]]      · simp only [x₀, log_exp]        rw [← Int.natCast_floor_eq_floor (div_nonneg (by linarith) (log_nonneg (by norm_num)))]        rfl