FKS2.theorem_3

@[blueprint  "fks2-theorem-3"  (title := "FKS2 Theorem 3")  (statement := /--  If $B \geq \max(3/2, 1 + C^2/16 R)$, $x_0 > 0$, and one has an admissible asymptotic bound  with parameters $A,B,C,x_0$ for $E_\theta$, and  $$ x_1 \geq \max( x_0, \exp( (1 + \frac{C}{2\sqrt{R}})^2 )),$$  then  $$ E_\pi(x) \leq \epsilon_{\theta,asymp}(x) ( 1 + \mu_{asymp}(x_0,x_1) ) $$  for all $x \geq x_1$.  In other words, we have an admissible bound with parameters  $(1+\mu_{asymp}(x_0,x_1))A, B, C, x_1$ for $E_\pi$.  -/)  (proof := /-- The starting point is Sublemma \ref{fks2-eq-30}.  The assumption ($\varepsilon_{\theta,\mathrm{asymp}}(x)$ provides an admissible bound on $\theta(x)$ for all $x \geq x_0$) to bound $\frac{\theta(x) - x}{\log(x)}$ and Lemma \ref{fks2-lemma-12} to bound $\int_{x_0}^{x} \frac{\theta(t) - t}{t (\log(t))^2} dt$.  We obtain  $$ |\pi(x) - \Li(x)| \leq |\pi(x_0) - \Li(x_0) - \frac{\theta(x_0) - x_0}{\log(x_0)}| + \frac{x \varepsilon_{\theta,\mathrm{asymp}}(x)}{\log(x)} + \frac{2 A_\theta}{R^B} x m(x_0,x) \exp(-C \sqrt{\frac{\log x}{R}}) D_+\left( \sqrt{\log x} - \frac{C}{2\sqrt{R}} \right).$$  We recall that $x \geq x_1 \geq x_0$.  Note that, by Corollary \ref{fks2-corollary-11},  $$ \frac{\log(x)}{x \varepsilon_{\theta,\mathrm{asymp}}(x)} = \frac{1}{A_\theta} g(1, 1 - B, \frac{C}{\sqrt{R}}, x) $$  is decreasing for all $x$.  Thus,  $$ \frac{\log(x)}{x \varepsilon_{\theta,\mathrm{asymp}}(x)} \leq \frac{\log(x_1)}{x_1 \varepsilon_{\theta,\mathrm{asymp}}(x_1)}. $$  In addition, we have the simplification  $$ \frac{\log(x)}{x \varepsilon_{\theta,\mathrm{asymp}}(x)} \frac{2 A_\theta}{R^B} x m(x_0,x) e^{-C \sqrt{\frac{\log x}{R}}} = 2 m(x_0,x) (\log(x))^{1 - B} = 2 (\log(x))^{1 - B} \leq 2 (\log(x_1))^{1 - B}, $$  by Definition \ref{classical-bound-theta} and by $m(x_0,x) = (\log(x))^{(2B - 3)/2}$, since $B \geq 3/2$.  Finally, since $\sqrt{\log(x_1)} - \frac{C}{2\sqrt{R}} > 1$, the Dawson function decreases for all $x \geq x_1$:  $$ D_+\left( \sqrt{\log x} - \frac{C}{2\sqrt{R}} \right) \leq D_+\left( \sqrt{\log x_1} - \frac{C}{2\sqrt{R}} \right). $$  We conclude by combining the above:  $$ \frac{|\pi(x) - \Li(x)|}{\frac{x \varepsilon_{\theta,\mathrm{asymp}}(x)}{\log(x)}} \leq \frac{\log(x_1)}{x_1 \varepsilon_{\theta,\mathrm{asymp}}(x_1)} |\pi(x_0) - \Li(x_0) - \frac{\theta(x_0) - x_0}{\log(x_0)}| + 1 + \frac{2 D_+\left( \sqrt{\log x_1} - \frac{C}{2\sqrt{R}} \right)}{\sqrt{\log(x_1)}}, $$  from which we deduce the announced bound. -/)  (latexEnv := "theorem")  (discussion := 675)]theorem theorem_3 (A B C R x₀ x₁ : ℝ)  (hB : B ≥ max (3 / 2) (1 + C ^ 2 / (16 * R)))  (hx0 : x₀ > 0)  (hE_theta : Eθ.classicalBound A B C R x₀)  (hx1 : x₁ ≥ max x₀ (exp ((1 + C / (2 * sqrt R)) ^ 2)))  (hR : R > 0)  (hA : A > 0)  (hx0_ge2 : x₀ ≥ 2)  (hsqrt_cond : 0 ≤ √(log x₀) - C / (2 * √R)) :  Eπ.classicalBound (A * (1 + μ_asymp A B C R x₀ x₁)) B C R x₁ := by  /-NOTE: The conditions hx0_ge2 and hsqrt_cond are not present in the source material [FKS2]. They are added to  facilitate the application of lemma_12, which requires x₀ ≥ 2 and 0 ≤ √(log x₀) - C/(2√R).  -/  obtain ⟨hx1x0, hx1_exp, hB1, hB2⟩ := theorem_3_easy_preconditions B C R x₀ x₁ hB hx1  have hx1_ge1 : x₁ ≥ 1 := le_trans (Real.one_le_exp (sq_nonneg _)) hx1_exp  have hx1_gt1 : x₁ > 1 := by linarith  have hlogx0 : log x₀ > 0 := Real.log_pos (by linarith)  intro x hx  simp only [admissible_bound_mul]  have h30 := eq_30 (show x ≥ x₀ by linarith) hx0_ge2  have hEtheta_x := hE_theta x (show x ≥ x₀ by linarith)  have hdelta := delta_term_bound hB2 hR hA hx1_gt1 hx hx0 hlogx0  have hintegral := integral_term_bound hB1 hR hA hE_theta hx1_gt1 hx1x0 hx hx0_ge2 hsqrt_cond hx1_exp  calc Eπ x ≤ Eθ x + (log x / x) * (x₀ / log x₀) * δ x₀ + (log x / x) * ∫ t in x₀..x, Eθ t / log t ^ 2 := h30    _ ≤ admissible_bound A B C R x +          ((x₀ * log x₁) / (admissible_bound A B C R x₁ * x₁ * log x₀) * δ x₀ *           admissible_bound A B C R x) +          (2 * dawson (√(log x₁) - C / (2 * √R)) / √(log x₁) *           admissible_bound A B C R x) := by linarith    _ = (1 + μ_asymp A B C R x₀ x₁) * admissible_bound A B C R x := by          unfold μ_asymp; ring