FKS2.corollary_21

@[blueprint  "fks2-corollary-21"  (title := "FKS2 Corollary 21")  (statement := /--  Let $B \geq \max(\frac{3}{2}, 1 + \frac{C^2}{16R})$ and $B > C^2/8R$.  Let $x_0, x_1 > 0$ with  $x_1 \geq \max(x_0, \exp( (1 + \frac{C}{2\sqrt{R}})^2))$. If $E_\psi$ satisfies an admissible  classical bound with parameters $A_\psi,B,C,R,x_0$, then $E_\pi$ satisfies an admissible  classical bound with $A_\pi, B, C, R, x_1$, where  $$ A_\pi = (1 + \nu_{asymp}(x_0)) (1 + \mu_{asymp}(x_0, x_1)) A_\psi$$  for all $x \geq x_0$, where  $$ |E_\theta(x)| \leq \varepsilon_{\theta,asymp}(x) :=    A (1 + \mu_{asymp}(x_0,x)) \exp(-C \sqrt{\frac{\log x}{R}})$$  where  $$ \nu_{asymp}(x_0) = \frac{1}{A_\psi} (\frac{R}{\log x_0})^B    \exp(C \sqrt{\frac{\log x_0}{R}}) (a_1 (\log x_0) x_0^{-1/2} + a_2 (\log x_0) x_0^{-2/3})$$  and  $$ \mu_{asymp}(x_0,x_1) = \frac{x_0 \log x_1}{\eps_{\theta,asymp}(x_1)x_1 \log x_0}    |E_\pi(x_0) - E_\theta(x_0)| + \frac{2 D_+\bigl(\sqrt{\log x_1} - \frac{C}{2\sqrt{R}}\bigr)}    {\sqrt{\log x_1}}.$$  -/)  (proof := /-- This follows by applying Theorem \ref{fks2-theorem-3} with Proposition \ref{fks2-proposition-13}.  The hypothesis $B > C^2/8R$ is not present in original source.-/)  (latexEnv := "corollary")  (discussion := 720)]theorem corollary_21  (Aψ B C R x₀ x₁ : ℝ)  (hB : B ≥ max (3 / 2) (1 + C ^ 2 / (16 * R)))  (hB' : B > C ^ 2 / (8 * R))  (hx0 : x₀ > 0)  (hx1 : x₁ ≥ max x₀ (exp ((1 + C / (2 * sqrt R)) ^ 2)))  (hEψ : Eψ.classicalBound Aψ B C R x₀)  (hR : R > 0)  (hAψ : Aψ > 0)  (hx0_ge2 : x₀ ≥ 2)  (hsqrt_cond : 0 ≤ √(log x₀) - C / (2 * √R))  (hx₀_ge7 : 7 ≤ Real.log x₀) :  let Aθ := Aψ * (1 + ν_asymp Aψ B C R x₀)  Eπ.classicalBound (Aθ * (1 + (μ_asymp Aθ B C R x₀ x₁))) B C R x₁ :=  -- NOTE: the hypothesis hB' is not present in the original source material [FKS2]. See  -- https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/720 for more information  -- NOTE: The hypotheses `hx0_ge2` and `hsqrt_cond` are also not present in [FKS2]. They are added  -- to facilitate theorem_3, which also had them added due to lemma_12.  let Aθ := Aψ * (1 + ν_asymp Aψ B C R x₀)  have hlogpos: 0 < log x₀ := by exact log_pos (show 1 < x₀ by linarith [hx0_ge2])  have hBKLNW1pos: BKLNW.a₁ (log x₀) > 0 := by    simp only [BKLNW.a₁]    unfold BKLNW.Inputs.a₁    split_ifs    · have : 0 < log BKLNW.Inputs.default.x₁ := by linarith [BKLNW.Inputs.default.hx₁]      linarith [BKLNW.Inputs.default.epsilon_nonneg this.le]    · have : 0 < log x₀ / 2 := by linarith      linarith [BKLNW.Inputs.default.epsilon_nonneg this.le]  have hBKLNW2pos : BKLNW.a₂ (log x₀) ≥ 0 := by    simp only [BKLNW.a₂]    unfold BKLNW.Inputs.a₂    have hf_pos (x : ℝ) (hx : x ≥ 0) : BKLNW.f x ≥ 0 := by      unfold BKLNW.f      apply Finset.sum_nonneg      intro n hn      apply rpow_nonneg hx    have hα_pos : 0 < BKLNW.Inputs.default.α := by      apply mul_pos <;> norm_num    have hterm1: 0 ≤ 1 + BKLNW.Inputs.default.α := by linarith    have hterm2: 0 ≤ max (BKLNW.f (rexp (log x₀))) (BKLNW.f (2 ^ (⌊log x₀ / log 2⌋₊ + 1))) := by exact le_max_iff.mpr (Or.inl (hf_pos (exp (log x₀)) (exp_nonneg _)))    nlinarith [hterm1, hterm2]  have hpostemp: 1 / Aψ * (R / log x₀) ^ B * exp (C * √(log x₀ / R)) > 0 := by positivity [hAψ, log_pos (show 1 < x₀ by linarith [hx0_ge2])]  have hν_asymp_pos: ν_asymp Aψ B C R x₀ > 0 := by unfold ν_asymp; apply (mul_pos_iff_of_pos_left hpostemp).2; positivity [hBKLNW1pos, hBKLNW2pos]  have hAθ : Aθ > 0 := by nlinarith [hAψ, hν_asymp_pos]  theorem_3 Aθ B C R x₀ x₁ hB hx0 (proposition_13 Aψ B C R x₀ hAψ hR hx0 hx₀_ge7 hEψ hB') hx1 hR hAθ hx0_ge2 hsqrt_cond