BKLNW.bklnw_lemma_9

@[blueprint  "bklnw-lemma-9"  (title := "BKLNW Lemma 9")  (statement := /-- Let $1 \le u < v$. Assume there exist $c = c_{u,v} > 0$ and $C= C_{u,v} > 0$ such that \begin{equation} \label{equ:c-Psi-C}  -c \le \frac{x - \psi(x)}{\sqrt{x}} \le C \qquad \text{for every }x \in [u,v].  \end{equation}Assume that there exists $c_0>0$ such that \begin{equation}\label{defn1:c0}  \psi(x) < c_0 x \text{ for all } x > 0.  \end{equation}If $u^2 < v$, then  \begin{equation}  \label{eqn:C-Section-Post-Lemma}  \theta(x) \ge x - (C + 1)x^{\frac12} - c_0 x^\frac13 - c x^{\frac14} - c_0 x^\frac15 \  \text{ for all } x \in [u^2,v].  \end{equation}-/)  (proof := /-- From Theorem \ref{costa-pereira-theorem-1a} we have \[  \psi(x) - \theta(x) \le \psi(x^{\frac12}) + \psi(x^{\frac13}) + \psi(x^{\frac15})\  \text{ for all } x >0. \] Together with \eqref{defn1:c0}, it follows \[  \psi(x) - \theta(x) \le \psi(x^{\frac12}) +  c_0 x^{\frac13} +c_0 x^{\frac15}  \text{ for all } x \in [u,v].\] -/)  (latexEnv := "lemma")  (discussion := 1260)]theorem bklnw_lemma_9 (u v : ℝ) (c C c₀ : ℝ)  (huv : 1 ≤ u ∧ u < v)  (hψ_bound : ∀ x ∈ Set.Icc u v, -c ≤ (x - ψ x) / sqrt x ∧ (x - ψ x) / sqrt x ≤ C)  (hψ_linear : ∀ x > 0, ψ x < c₀ * x) :  ∀ x ∈ Set.Icc (u ^ 2) v, θ x ≥ x - (C + 1) * x ^ (1 / 2 : ℝ) - c₀ * x ^ (1 / 3 : ℝ) - c * x ^ (1 / 4 : ℝ) - c₀ * x ^ (1 / 5 : ℝ) := by  intro x hx_mem  have hx_lb : u ^ 2 ≤ x := hx_mem.1  have hx_ub : x ≤ v := hx_mem.2  have hx_pos : (0 : ℝ) < x := by    have : (0 : ℝ) < u := by linarith [huv.1]    nlinarith  have hx_ge_u : u ≤ x := by nlinarith [huv.1, hx_lb]  have hx_in_uv : x ∈ Set.Icc u v := ⟨hx_ge_u, hx_ub⟩  have hxhalf_ge_u : u ≤ x ^ (1 / 2 : ℝ) := by    rw [← Real.sqrt_eq_rpow]    exact (Real.sqrt_sq (by linarith [huv.1])).symm.trans_le (Real.sqrt_le_sqrt hx_lb)  have hxhalf_le_v : x ^ (1 / 2 : ℝ) ≤ v := by    rw [← Real.sqrt_eq_rpow]    have hv_ge1 : 1 < v := by nlinarith [huv.1]    have hsqrtv : Real.sqrt v ≤ v := by      rw [Real.sqrt_le_left (by linarith)]; nlinarith    exact (Real.sqrt_le_sqrt hx_ub).trans hsqrtv  have hCP : ψ 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ψx_lb : x - C * x ^ (1 / 2 : ℝ) ≤ ψ x := by    have hbound := (hψ_bound x hx_in_uv).2    rw [div_le_iff₀ (Real.sqrt_pos.mpr hx_pos), Real.sqrt_eq_rpow] at hbound    linarith  have hψxhalf_ub : ψ (x ^ (1 / 2 : ℝ)) ≤ x ^ (1 / 2 : ℝ) + c * x ^ (1 / 4 : ℝ) := by    have hbound := (hψ_bound _ ⟨hxhalf_ge_u, hxhalf_le_v⟩).1    have hsqrt_rw : Real.sqrt (x ^ (1 / 2 : ℝ)) = x ^ (1 / 4 : ℝ) := by      rw [Real.sqrt_eq_rpow, ← Real.rpow_mul hx_pos.le]; norm_num    rw [le_div_iff₀ (Real.sqrt_pos.mpr (Real.rpow_pos_of_pos hx_pos _)),        hsqrt_rw] at hbound    linarith  have hψxthird_ub : ψ (x ^ (1 / 3 : ℝ)) < c₀ * x ^ (1 / 3 : ℝ) :=    hψ_linear _ (Real.rpow_pos_of_pos hx_pos _)  have hψxfifth_ub : ψ (x ^ (1 / 5 : ℝ)) < c₀ * x ^ (1 / 5 : ℝ) :=    hψ_linear _ (Real.rpow_pos_of_pos hx_pos _)  calc θ x      ≥ ψ x - ψ (x ^ (1/2 : ℝ)) - ψ (x ^ (1/3 : ℝ)) - ψ (x ^ (1/5 : ℝ)) := by linarith    _ ≥ (x - C * x ^ (1/2 : ℝ))          - (x ^ (1/2 : ℝ) + c * x ^ (1/4 : ℝ))          - c₀ * x ^ (1/3 : ℝ)          - c₀ * x ^ (1/5 : ℝ)                     := by linarith    _ = x - (C + 1) * x ^ (1/2 : ℝ)          - c₀ * x ^ (1/3 : ℝ)          - c * x ^ (1/4 : ℝ)          - c₀ * x ^ (1/5 : ℝ)                     := by ring