BKLNW_app.bklnw_lemma_15

@[blueprint  "bklnw-lemma_15"  (title := "Lemma 15")  (statement := /-- Let $B_0$, $B$, and $c$ be  positive constants such that\begin{equation}\tag{A.27}\label{bklnw:A.27}|(x-\psi(x))/\sqrt{x}| \leq c\hbox{ for all } B_0 < x \leq B\end{equation}  is known.  Furthermore, assume for every  $b_0 > 0$ there exists $\varepsilon(b_0) > 0$  such that\begin{equation}\tag{A.28}\label{bklnw:A.28}|\psi(x) - x| \leq \varepsilon(b_0) x\quad \text{for all } x \geq e^{b_0}.\end{equation}Let $b$ be positive such that$e^b \in (B_0, B]$. Then, for all$x \geq e^b$ we have\begin{equation}\tag{A.29}\label{bklnw:A.29}\left|\frac{\psi(x) - x}{x}\right|\leq \max (\frac{c}{e^{\frac{b}{2}}},\varepsilon(\log B)).\end{equation} -/)  (proof := /-- Multiplying both sides of  \eqref{bklnw:A.27} by $\frac{1}{\sqrt{x}}$ gives\[\left|\frac{\psi(x) - x}{x}\right|\leq \frac{c}{e^{\frac{b}{2}}}\quad \text{for all } e^b \leq x \leq B\]as $\frac{1}{\sqrt{x}}\leq \frac{1}{e^{\frac{b}{2}}}$.Then, for $x \geq B$ we apply \eqref{bklnw:A.28}with $b_0 = \log B$.Combining these bounds,we derive \eqref{bklnw:A.29}. -/)  (latexEnv := "lemma")  (discussion := 753)]theorem bklnw_lemma_15 (c B₀ B : ℝ)    (hbound : ∀ x ∈ Set.Ioc B₀ B,      Eψ x ≤ c / sqrt x)    (ε : ℝ → ℝ)    (hε : ∀ b₀ > 0, ∀ x ≥ exp b₀, Eψ x ≤ ε b₀)    (b : ℝ)    (hb : exp b ∈ Set.Ioc B₀ B)    (hbpos : b > 0)    (hcpos : c > 0)    (hBpos : B > 0) :    ∀ x ≥ exp b,      Eψ x ≤ max (c / exp (b / 2))        (ε (log B)) := by  intro x hx  by_cases! hcases : x ≤ B  · have hlb : B₀ < x := by linarith [hx, hb.1]    simp only [Set.Ioc, Set.mem_setOf_eq, and_imp] at hbound    have hb : Eψ x ≤ c / sqrt x :=      hbound x hlb hcases    have hsqrtcomp : sqrt (exp b) ≤ sqrt x :=      Real.sqrt_monotone hx    have hidentity1 : exp (2 * (b / 2)) = exp (b / 2) ^ 2 := Real.exp_nat_mul (b / 2) 2    have hidentity2 : 2 * (b / 2) = b := by ring    simp only [hidentity2] at hidentity1    have hnonneg : 0 ≤ exp (b / 2) := by      positivity    have hidentity3 : sqrt (exp b) = sqrt (exp (b / 2) ^ 2) := by      simpa using congrArg Real.sqrt hidentity1    simp only [Real.sqrt_sq hnonneg] at hidentity3    have hsqrtcomp2 : exp (b / 2) ≤ sqrt x := by      linarith    have hsqrtpos : sqrt x > 0 := by      linarith [exp_pos (b / 2)]    have hsqrtcomp3 : c / sqrt x ≤ c / exp (b / 2) := by gcongr    have hubcomp : c / exp (b / 2) ≤ max (c / exp (b / 2)) (ε (log B)) := le_max_left ..    linarith  · have hidentity : exp (log B) = B :=      Real.exp_log hBpos    have hBone : 1 < B := by      linarith [hb.2, Real.one_lt_exp_iff.2 hbpos]    have hlogBpos : 0 < log B :=      Real.log_pos hBone    specialize hε (log B) hlogBpos    have hlb : x ≥ exp (log B) := by linarith    specialize hε x hlb    have hubcomp : ε (log B) ≤ max (c / exp (b / 2)) (ε (log B)) := le_max_right ..    linarith