FKS2.proposition_17

@[blueprint  "fks2-proposition-17"  (title := "FKS2 Proposition 17")  (statement := /--  Let $x > x_0 > 2$.  If $E_\psi(x) \leq \varepsilon_{\psi,num}(x_0)$, then  $$ - \varepsilon_{\theta,num}(x_0) \leq \frac{\theta(x)-x}{x}    \leq \varepsilon_{\psi,num}(x_0) \leq \varepsilon_{\theta,num}(x_0)$$  where  $$ \varepsilon_{\theta,num}(x_0) = \varepsilon_{\psi,num}(x_0) +    1.00000002(x_0^{-1/2}+x_0^{-2/3}+x_0^{-4/5}) +    0.94 (x_0^{-3/4} + x_0^{-5/6} + x_0^{-9/10})$$ -/)  (proof := /-- The upper bound is immediate since $\theta(x) \leq \psi(x)$ for all $x$. For the lower bound, we have  $$\frac{\theta(x) - x}{x} = \frac{\psi(x) - x}{x} + \frac{\theta(x) - \psi(x)}{x}.$$  By Theorem \ref{costa-pereira-theorem-1a}, we have  $$\psi(x) - \theta(x) \leq \psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5}).$$  We use \cite[Theorem 2]{Buthe}, that for $0 < x < 11$, $\psi(x) < x$, and that $\varepsilon_{\psi,num}(10^{19}) < 2 \cdot 10^{-8}$. In particular when $2 < x < 10^{38}$,  $$\psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5}) \leq x^{1/2} + x^{1/3} + x^{1/5} + 0.94(x^{1/4} + x^{1/6} + x^{1/10}),$$  when $10^{38} \leq x < 10^{54}$,  $$\psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5}) \leq 1.00000002x^{1/2} + x^{1/3} + x^{1/5} + 0.94(x^{1/6} + x^{1/10}),$$  when $10^{54} \leq x < 10^{95}$,  $$\psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5}) \leq 1.00000002(x^{1/2} + x^{1/3}) + x^{1/5} + 0.94x^{1/10},$$  and finally when $x \geq 10^{95}$,  $$\psi(x^{1/2}) + \psi(x^{1/3}) + \psi(x^{1/5}) \leq 1.00000002(x^{1/2} + x^{1/3} + x^{1/5}).$$  The result follows by combining the worst coefficients from all cases and dividing by $x$. -/)  (latexEnv := "proposition")  (discussion := 711)]theorem proposition_17 {x x₀ : ℝ} (hx : x > x₀) (hx₀ : x₀ > 2) (εψ : ℝ → ℝ) (hEψ : Eψ x ≤ εψ x₀) :    -εθ_from_εψ εψ x₀ ≤ (θ x - x) / x ∧ (θ x - x) / x ≤ εψ x₀ ∧ εψ x₀ ≤ εθ_from_εψ εψ x₀ := by  refine ⟨?_, ?_, ?_⟩  · have hx_pos : 0 < x := by linarith    have hθ_bound :        θ x ≥ x - εψ x₀ * x -          1.00000002 * (x ^ (1 / 2 : ℝ) + x ^ (1 / 3 : ℝ) + x ^ (1 / 5 : ℝ)) -          0.94 * (x ^ (1 / 4 : ℝ) + x ^ (1 / 6 : ℝ) + x ^ (1 / 10 : ℝ)) := by      have hθ_from_ψ :          θ x ≥ x - εψ x₀ * x -            (ψ (x ^ (1 / 2 : ℝ)) + ψ (x ^ (1 / 3 : ℝ)) + ψ (x ^ (1 / 5 : ℝ))) := by        have hθ_basic : θ x ≥ x - εψ x₀ * x - (ψ x - θ x) := by          rw [show Eψ x = |ψ x - x| / x from rfl] at hEψ          rw [div_le_iff₀] at hEψ <;>            cases abs_cases (ψ x - x) <;> nlinarith [show 0 < x by linarith]        exact hθ_basic.trans' <| sub_le_sub_left          (le_trans (by norm_num)            (show ψ x - θ x ≤ ψ (x ^ (1 / 2 : ℝ)) + ψ (x ^ (1 / 3 : ℝ)) + ψ (x ^ (1 / 5 : ℝ)) by              simpa [one_div] using Chebyshev.psi_sub_theta_le_psi_add_psi_add_psi x)) _      have hψ_bounds :          ψ (x ^ (1 / 2 : ℝ)) ≤ 1.00000002 * x ^ (1 / 2 : ℝ) + 0.94 * x ^ (1 / 4 : ℝ) ∧          ψ (x ^ (1 / 3 : ℝ)) ≤ 1.00000002 * x ^ (1 / 3 : ℝ) + 0.94 * x ^ (1 / 6 : ℝ) ∧          ψ (x ^ (1 / 5 : ℝ)) ≤ 1.00000002 * x ^ (1 / 5 : ℝ) + 0.94 * x ^ (1 / 10 : ℝ) := by        have hψ_le : ∀ y : ℝ, 1 < y → ψ y ≤ 1.00000002 * y + 0.94 * y ^ (1 / 2 : ℝ) :=          fun y a ↦ psi_le_bound y a        exact ⟨by            convert hψ_le (x ^ (1 / 2 : ℝ)) (one_lt_rpow (by linarith) (by norm_num)) using 1            rw [← rpow_mul (by linarith)]; norm_num, by            convert hψ_le (x ^ (1 / 3 : ℝ)) (one_lt_rpow (by linarith) (by norm_num)) using 1            rw [← rpow_mul (by linarith)]; norm_num, by            convert hψ_le (x ^ (1 / 5 : ℝ)) (one_lt_rpow (by linarith) (by norm_num)) using 1            rw [← rpow_mul (by linarith)]; norm_num⟩      linarith [rpow_pos_of_pos hx_pos (1 / 2 : ℝ),        rpow_pos_of_pos hx_pos (1 / 3 : ℝ), rpow_pos_of_pos hx_pos (1 / 5 : ℝ),        rpow_pos_of_pos hx_pos (1 / 4 : ℝ), rpow_pos_of_pos hx_pos (1 / 6 : ℝ),        rpow_pos_of_pos hx_pos (1 / 10 : ℝ)]    have hfactor :        1.00000002 * (x ^ (1 / 2 : ℝ) + x ^ (1 / 3 : ℝ) + x ^ (1 / 5 : ℝ)) +          0.94 * (x ^ (1 / 4 : ℝ) + x ^ (1 / 6 : ℝ) + x ^ (1 / 10 : ℝ)) ≤        x * (1.00000002 * (x₀ ^ (-(1 / 2 : ℝ)) + x₀ ^ (-(2 / 3 : ℝ)) + x₀ ^ (-(4 / 5 : ℝ))) +          0.94 * (x₀ ^ (-(3 / 4 : ℝ)) + x₀ ^ (-(5 / 6 : ℝ)) + x₀ ^ (-(9 / 10 : ℝ)))) := by      have hpowers :          x ^ (1 / 2 : ℝ) ≤ x * x₀ ^ (-(1 / 2 : ℝ)) ∧          x ^ (1 / 3 : ℝ) ≤ x * x₀ ^ (-(2 / 3 : ℝ)) ∧          x ^ (1 / 5 : ℝ) ≤ x * x₀ ^ (-(4 / 5 : ℝ)) ∧          x ^ (1 / 4 : ℝ) ≤ x * x₀ ^ (-(3 / 4 : ℝ)) ∧          x ^ (1 / 6 : ℝ) ≤ x * x₀ ^ (-(5 / 6 : ℝ)) ∧          x ^ (1 / 10 : ℝ) ≤ x * x₀ ^ (-(9 / 10 : ℝ)) := by        have hpower_bound : ∀ k : ℝ, 0 < k → k < 1 → x ^ k ≤ x * x₀ ^ (k - 1) := by          intro k hk hk'          rw [← log_le_log_iff (rpow_pos_of_pos (by linarith) _) (mul_pos (by linarith)            (rpow_pos_of_pos (by linarith) _)), log_rpow (by linarith),              log_mul (by linarith) (ne_of_gt (rpow_pos_of_pos (by linarith) _)), log_rpow (by linarith)]          ring_nf          nlinarith [log_lt_log (by linarith) hx]        exact ⟨by convert hpower_bound (1 / 2) (by norm_num) (by norm_num) using 1; ring_nf,          by convert hpower_bound (1 / 3) (by norm_num) (by norm_num) using 1; ring_nf,          by convert hpower_bound (1 / 5) (by norm_num) (by norm_num) using 1; ring_nf,          by convert hpower_bound (1 / 4) (by norm_num) (by norm_num) using 1; ring_nf,          by convert hpower_bound (1 / 6) (by norm_num) (by norm_num) using 1; ring_nf,          by convert hpower_bound (1 / 10) (by norm_num) (by norm_num) using 1; ring_nf⟩      linarith [rpow_pos_of_pos hx_pos (1 / 2 : ℝ),        rpow_pos_of_pos hx_pos (1 / 3 : ℝ), rpow_pos_of_pos hx_pos (1 / 5 : ℝ),        rpow_pos_of_pos hx_pos (1 / 4 : ℝ), rpow_pos_of_pos hx_pos (1 / 6 : ℝ),        rpow_pos_of_pos hx_pos (1 / 10 : ℝ)]    rw [le_div_iff₀ hx_pos, εθ_from_εψ]    grind  · have h_le_psi : (θ x - x) / x ≤ (ψ x - x) / x := by      gcongr      · linarith      · exact theta_le_psi x    exact h_le_psi.trans <| hEψ.trans' (div_le_div_of_nonneg_right (le_abs_self _) (by linarith))  · exact le_add_of_le_of_nonneg (le_add_of_nonneg_right <| by positivity) <| by positivity