FKS2.hasDerivAt_Li_sub_div_log

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]

private lemma Li_ibp {x : ℝ} (hx : x > 2) : Li x - x / log x = -2 / log 2 + ∫ t in (2:ℝ)..x, 1 / (log t) ^ 2 := by have h_parts : ∀ a b : ℝ, 2 ≤ a → a < b → ∫ t in a..b, (1 : ℝ) / Real.log t = (b / Real.log b) - (a / Real.log a) + ∫ t in a..b, (1 : ℝ) / Real.log t ^ 2 := by intro a b _ _ rw [intervalIntegral.integral_eq_sub_of_hasDerivAt] rotate_right next => use fun x => x / Real.log x + ∫ t in a..x, 1 / Real.log t ^ 2 · norm_num; ring · intro x hx exact Ramanujan.hasDerivAt_li_antideriv (by linarith) (by cases Set.mem_uIcc.mp hx <;> linarith) · apply_rules [ContinuousOn.intervalIntegrable] exact continuousOn_of_forall_continuousAt fun t ht => ContinuousAt.div continuousAt_const (Real.continuousAt_log (by cases Set.mem_uIcc.mp ht <;> linarith)) (ne_of_gt (Real.log_pos (by cases Set.mem_uIcc.mp ht <;> linarith))) convert! congr_arg (fun y => y - x / Real.log x) (h_parts 2 x (by norm_num) hx) using 1 ring!

/-The following lemmas are used for the proof of lemma_20_b. The first lemma was originally used for the proof of theorem_6_3, but was moved up here to be used for lemma_20_b as well.