FKS2.theorem_6_2

@[blueprint  "fks2-theorem-6-2"  (title := "FKS2 Theorem 6, substep 2")  (statement := /-- With the above hypotheses, for all $x \geq x_1$ we have  $$ \frac{\log x}{x} \int_{x_1}^x \frac{dt}{\log^2 t} < \frac{1}{\log x_1 + \log \log x_1 - 1}. $$ -/)  (proof := /-- Call the left-hand side $f(x)$. We have  $$ f(x) = \frac{\log x}{x} \left( \mathrm{Li}(x) - \frac{x}{\log x} - \mathrm{Li}(x_1) + \frac{x_1}{\log x_1} \right). $$  Using integration by parts, its derivative can be written as  $$ f'(x) = -\frac{1}{x \log^2 x} + \frac{2}{x \log^3 x} + \frac{\log x - 1}{x^2} \left( \frac{x_1}{\log^2 x_1} + \frac{2 x_1}{\log^3 x_1} - \int_{x_1}^x \frac{6}{\log^4 t} dt \right). $$  From which we see that $f'(x_1) = \frac{1}{\log x_1} > 0$, and that $f'(x)$ is eventually negative. Thus there exists a critical point for $f(x)$ to the right of $x_1$. Moreover, by bounding $\int_{x_1}^x \frac{6}{\log^4 t} dt < 6 \frac{x - x_1}{\log^4 x_1}$, one finds that $f'(x_1 \log x_1) > 0$ if $x_1 > e$.  Now we write $f'(x) = \frac{f_1(x)}{x^2}$ with  $$ f_1(x) = \frac{x}{\log x} - (\log x - 1) \int_{x_1}^x \frac{1}{\log^2 t} dt. $$  Its derivative is $f_1'(x) = -\frac{1}{x} \int_{x_1}^x \frac{1}{\log^2 t} dt$, which is negative for $x > x_1$. Thus $f_1(x)$ decreases and vanishes at most once, giving $f(x)$ at most one critical point, $x_m > x_1$, which is then the maximum of $f(x)$. In other words, $x_m$ satisfies $f_1(x_m) = 0$, i.e.\ $\mathrm{Li}(x_m) - \mathrm{Li}(x_1) + \frac{x_1}{\log x_1} = -\frac{x_m}{1 - \log x_m}$, which shows that $f(x)$ attains its maximum at $x = x_m$, where  $$ f(x_m) = \frac{\log x_m}{x_m} \left( -\frac{x_m}{\log x_m} - \frac{x_m}{1 - \log x_m} \right) = \frac{1}{\log x_m - 1}. $$  Now, because $x_m > x_1 \log x_1$ we obtain the bound  $$ f(x) < \frac{1}{\log x_1 + \log(\log x_1) - 1}, $$  which gives the announced result.  -/)  (latexEnv := "sublemma")  (discussion := 716)]theorem theorem_6_2 {x₁ : ℝ} (h : x₁ ≥ 14) (x : ℝ) (hx : x ≥ x₁) :  (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2 < 1 / (log x₁ + log (log x₁) - 1) := by  have h_denom_pos : 0 < log x₁ + log (log x₁) - 1 := by    have hlog14 : log 14 ≤ log x₁ := Real.log_le_log (by norm_num) h    have hlog14_pos : 0 < log 14 := Real.log_pos (by norm_num)    linarith [Real.log_le_log hlog14_pos hlog14,              show (0 : ℝ) < log 14 + log (log 14) - 1 from by interval_decide]  rcases exists_isMaxOn_Ici_log_div_self_mul_integral_one_div_log_sq h with ⟨xm, hxm_gt, hxm_bound, h_max⟩  have h_log_sub_lt : log x₁ + log (log x₁) - 1 < log xm - 1 := by    have h1 : log x₁ > 1 := log_gt_one_of_ge_14 h    have h_log_mul : log (x₁ * log x₁) = log x₁ + log (log x₁) :=      Real.log_mul (by linarith : x₁ ≠ 0) (by linarith : log x₁ ≠ 0)    linarith [Real.log_lt_log (mul_pos (by linarith : 0 < x₁) (by linarith : 0 < log x₁)) hxm_bound,              h_log_mul]  calc (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2      ≤ 1 / (log xm - 1)                        := h_max x hx    _ < 1 / (log x₁ + log (log x₁) - 1)         := one_div_lt_one_div_of_lt h_denom_pos h_log_sub_lt