FKS2.lemma_20_a

@[blueprint  "fks2-lemma-20a"  (title := "FKS2 Lemma 20a")  (statement := /--  The function $\Li(x) - \frac{x}{\log x}$ is strictly increasing for $x > 6.58$.  -/)  (proof := /-- Differentiate  \[  \frac{d}{dx} \left( \Li(x) - \frac{x}{\log(x)} \right) = \frac{1}{\log(x)} + \frac{1 - \log(x)}{(\log(x))^2} = \frac{1}{(\log(x))^2}  \]  to see that the difference is strictly increasing. Evaluating at $x = 6.58$ and applying the mean value theorem gives the announced result.  -/)  (latexEnv := "lemma")  (discussion := 713)]theorem lemma_20_a : StrictMonoOn (fun x ↦ Li x - x / log x) (Set.Ioi 6.58) := by  have hpos (x : ℝ) (hx : x ∈ Set.Ioi 6.58) := log_pos (by linarith [Set.mem_Ioi.mp hx]) |>.ne'  apply strictMonoOn_of_deriv_pos (convex_Ioi _)  · apply HasDerivAt.continuousOn (by apply hasDerivAt_Li) |>.sub    fun_prop (disch := simp_all)  · intro x hx    rw [interior_Ioi, Set.mem_Ioi] at hx    rw [deriv_fun_sub (hasDerivAt_Li hx).differentiableAt (by fun_prop (disch := simp_all)),      deriv_fun_div differentiableAt_fun_id (differentiableAt_log (by linarith)) (hpos x hx)]    simp [(hasDerivAt_Li hx).deriv, field, pow_two_pos_of_ne_zero, (hpos x hx), - sub_pos]