FKS2.proposition_13

@[blueprint  "fks2-proposition-13"  (title := "FKS2 Proposition 13")  (statement := /--  Suppose that $A_\psi,B,C,R,x_0$ give an admissible bound for $E_\psi$.  If $B > C^2/8R$, then  $A_\theta, B, C, R, x_0$ give an admissible bound for $E_\theta$, where  $$ A_\theta = A_\psi (1 + \nu_{asymp}(x_0))$$  with  $$ \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 $a_1,a_2$ are given by Definitions \ref{bklnw-def-a-1} and \ref{bklnw-def-a-2}.  -/)  (proof := /-- The proof of Corollary \ref{bklnw-cor-14-1} essentially proves the proposition, but requires that $x_0 \geq e^{1000}$ to conclude that the function  $$ 1 + \frac{a_1 \exp(C \sqrt{\frac{\log x}{R}})}{A_\psi \sqrt{x} (\log x/R)^{B}} + \frac{a_2 \exp(C \sqrt{\frac{\log x}{R}})}{A_\psi x^{2/3} (\log x/R)^{B}} = 1 + \frac{a_1}{A_\psi} g(1/2, -B, C/\sqrt{R}, x) + \frac{a_2}{A_\psi} g(2/3, -B, C/\sqrt{R}, x)$$  is decreasing. By Lemma \ref{fks2-lemma-10a}, since $B > C^2/8R$, the function is actually decreasing for all $x$. -/)  (latexEnv := "proposition")  (discussion := 671)]theorem proposition_13  (Aψ B C R x₀ : ℝ) (hAψ : Aψ > 0) (hR : R > 0) (hx₀_pos : 0 < x₀) (hx₀ : 7 ≤ Real.log x₀)  (h_bound : Eψ.classicalBound Aψ B C R x₀)  (hB : B > C ^ 2 / (8 * R)) :  Eθ.classicalBound (Aψ * (1 + ν_asymp Aψ B C R x₀)) B C R x₀ := by  unfold Eθ.classicalBound Eθ  intro x hx  have hx_pos : 0 < x := lt_of_lt_of_le hx₀_pos hx  have h_abs_le : |θ x - x| ≤ |ψ x - x| + (ψ x - θ x) := by    have h1 : |θ x - x| ≤ |ψ x - x| + |θ x - ψ x| := by      rw [show θ x - x = (ψ x - x) + (θ x - ψ x) by ring]; exact abs_add_le _ _    have h2 : |θ x - ψ x| = ψ x - θ x := by      rw [abs_sub_comm, abs_of_nonneg (sub_nonneg.mpr (theta_le_psi x))]    linarith  have hg1_anti : StrictAntiOn (g_bound (1 / 2) (-B) (C / sqrt R)) (Set.Ioi 1) :=    g_bound_strictAntiOn (1 / 2) (by norm_num) B C R hR      (by rw [show 16 * (1 / 2 : ℝ) * R = 8 * R by ring]; exact hB)  have hg2_anti : StrictAntiOn (g_bound (2 / 3) (-B) (C / sqrt R)) (Set.Ioi 1) :=    g_bound_strictAntiOn (2 / 3) (by norm_num) B C R hR (by      have : 0 ≤ C ^ 2 / R := by positivity      rw [show C ^ 2 / (16 * (2 / 3 : ℝ) * R) = (3 / 32) * (C ^ 2 / R) by ring]      rw [show C ^ 2 / (8 * R) = (1 / 8) * (C ^ 2 / R) by ring] at hB      linarith)  have hlog_pos : 0 < log x := log_pos (by    have : 1 < x₀ := by rw [← log_pos_iff hx₀_pos.le]; linarith    linarith)  have ha₁_nonneg : 0 ≤ BKLNW.a₁ (log x₀) := by    unfold BKLNW.a₁ BKLNW.Inputs.a₁; split_ifs    · have hx₁_ge_one : 1 ≤ BKLNW.Inputs.default.x₁ := (one_le_exp (by positivity)).trans BKLNW.Inputs.default.hx₁      have hε := BKLNW.Pre_inputs.epsilon_nonneg BKLNW.Inputs.default.toPre_inputs (Real.log_nonneg hx₁_ge_one)      linarith    · have hε := BKLNW.Pre_inputs.epsilon_nonneg BKLNW.Inputs.default.toPre_inputs (by linarith : 0 ≤ log x₀ / 2)      linarith  have ha₂_nonneg : 0 ≤ BKLNW.a₂ (log x₀) := by    unfold BKLNW.a₂ BKLNW.Inputs.a₂    refine mul_nonneg (by norm_num [BKLNW.Inputs.default, BKLNW_app.table_8_margin]) (le_trans ?_ (le_max_left _ _))    unfold BKLNW.f; exact Finset.sum_nonneg (fun _ _ ↦ by positivity)  have h_term1_le : BKLNW.a₁ (log x₀) * x ^ (1 / 2 : ℝ) / x ≤      admissible_bound Aψ B C R x * ((1 / Aψ) * (R / log x₀) ^ B * exp (C * sqrt (log x₀ / R)) *        (BKLNW.a₁ (log x₀) * log x₀ * x₀ ^ (-(1 / 2 : ℝ)))) := by    have h := mul_rpow_sub_div_le_admissible_bound_mul (1 / 2) _ Aψ B C R x x₀ ha₁_nonneg hAψ hR hx_pos hx₀_pos      hlog_pos (by linarith) hx₀ (g_bound_le_of_anti hg1_anti hx₀_pos hx₀ hx)    rwa [show (1 : ℝ) - 1 / 2 = 1 / 2 by norm_num] at h  have h_term2_le : BKLNW.a₂ (log x₀) * x ^ (1 / 3 : ℝ) / x ≤      admissible_bound Aψ B C R x * ((1 / Aψ) * (R / log x₀) ^ B * exp (C * sqrt (log x₀ / R)) *        (BKLNW.a₂ (log x₀) * log x₀ * x₀ ^ (-(2 / 3 : ℝ)))) := by    have h := mul_rpow_sub_div_le_admissible_bound_mul (2 / 3) _ Aψ B C R x x₀ ha₂_nonneg hAψ hR hx_pos hx₀_pos      hlog_pos (by linarith) hx₀ (g_bound_le_of_anti hg2_anti hx₀_pos hx₀ hx)    rwa [show (1 : ℝ) - 2 / 3 = 1 / 3 by norm_num] at h  calc |θ x - x| / x    _ ≤ (|ψ x - x| + (ψ x - θ x)) / x := div_le_div_of_nonneg_right h_abs_le hx_pos.le    _ ≤ admissible_bound Aψ B C R x + (ψ x - θ x) / x := by rw [add_div]; exact add_le_add_left (h_bound x hx) _    _ ≤ admissible_bound Aψ B C R x +        (admissible_bound Aψ B C R x * ((1 / Aψ) * (R / log x₀) ^ B * exp (C * sqrt (log x₀ / R)) *          (BKLNW.a₁ (log x₀) * log x₀ * x₀ ^ (-(1 / 2 : ℝ)))) +         admissible_bound Aψ B C R x * ((1 / Aψ) * (R / log x₀) ^ B * exp (C * sqrt (log x₀ / R)) *          (BKLNW.a₂ (log x₀) * log x₀ * x₀ ^ (-(2 / 3 : ℝ))))) := by        have h_div_le : (ψ x - θ x) / x ≤ (BKLNW.a₁ (log x₀) * x ^ (1 / 2 : ℝ) + BKLNW.a₂ (log x₀) * x ^ (1 / 3 : ℝ)) / x :=          div_le_div_of_nonneg_right (BKLNW.cor_5_1 hx₀ (by rwa [exp_log hx₀_pos])) hx_pos.le        rw [add_div] at h_div_le        linarith [h_term1_le, h_term2_le]    _ = admissible_bound (Aψ * (1 + ν_asymp Aψ B C R x₀)) B C R x := by        unfold admissible_bound ν_asymp; simp only [neg_div]; ring