BKLNW.thm_1a

@[blueprint  "bklnw-thm-1a"  (title := "BKLNW Theorem 1a")  (statement := /--  For any fixed $X_0 \geq 1$, there exists $m_0 > 0$ such that, for all $x \geq X_0$  $$ x(1 - m_0) \leq \theta(x). $$  For any fixed $X_1 \geq 1$, there exists $M_0 > 0$ such that, for all $x \geq X_1$  $$ \theta(x) \leq x(1 + M_0). $$  For $X_0, X_1 \geq e^{20}$, we have  $$ m_0 = \varepsilon(\log X_0) + 1.03883 \left( X_0^{-1/2} + X_0^{-2/3} + X_0^{-4/5} \right) $$  and  $$ M_0 = \varepsilon(\log X_1). $$  -/)  (proof := /-- Combine Lemmas \ref{bklnw-lemma-11a} with $b = \log X_1$ for the upper bound, and and \ref{bklnw-lemma-11b} with $b = \log X_0$ for the lower bound. -/)  (latexEnv := "theorem")  (discussion := 790)]theorem thm_1a {X₀ X₁ x : ℝ} (hX₀ : X₀ ≥ exp 20) (hX₁ : X₁ ≥ exp 20) (hx₀ : x ≥ X₀) (hx₁ : x ≥ X₁) :    let m₀ := Pre_inputs.default.ε (log X₀) + RS_prime.c₀ * (X₀^(-1/2:ℝ) + X₀^(-2/3:ℝ) + X₀^(-4/5:ℝ))    let M₀ := Pre_inputs.default.ε (log X₁)    x * (1 - m₀) ≤ θ x ∧ θ x ≤ x * (1 + M₀) := by  have hX₀' : X₀ > 1 := by linarith [add_one_le_exp 20]  have hX₁' : X₁ > 1 := by linarith [add_one_le_exp 20]  have h_psi_bounds : ψ x ≤ x * (1 + Pre_inputs.default.ε (log X₁)) := by    have := BKLNW_app.theorem_2 (log X₁) (log_nonneg hX₁'.le) x (by rw [exp_log (by linarith)]; linarith)    rw [mul_add, mul_one, abs_le] at *    linarith!  have h_theta_bounds : θ x ≥ (1 - Pre_inputs.default.ε (log X₀) -      RS_prime.c₀ * (exp (-log X₀ / 2) + exp (-2 * log X₀ / 3) +        exp (-4 * log X₀ / 5))) * x := by    grind [lemma_11b Pre_inputs.default (log_pos (hX₀')) ((exp_log (by positivity)).symm ▸ hx₀)]  refine ⟨?_, by grind [theta_le_psi x]⟩  convert h_theta_bounds.le using 1  grind [rpow_def_of_pos (by linarith : 0 < X₀)]