FKS2.deriv_log_div_self_mul_integral_one_div_log_sq_pos

lemma deriv_log_div_self_mul_integral_one_div_log_sq_pos {x₁ : ℝ} (h : x₁ ≥ 14) :    deriv (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2) (x₁ * log x₁) > 0 := by  have h_logx₁_gt : 1 < Real.log x₁ := log_gt_one_of_ge_14 h  have ht₀_pos : 0 < x₁ * log x₁ := mul_pos (by linarith) (by linarith)  have hx₁_le_x₀ : x₁ ≤ x₁ * Real.log x₁ := x1_le_x1_log_x1 h  have h_deriv_t₀ := hasDerivAt_log_div_self_mul_integral (by linarith : 1 < x₁) (by nlinarith : x₁ < x₁ * log x₁)  rw [h_deriv_t₀.deriv]  have ht₀_sq_pos : 0 < (x₁ * log x₁) ^ 2 := pow_pos ht₀_pos 2  refine div_pos ?_ ht₀_sq_pos  have ht₀_mem : x₁ * log x₁ ∈ Set.Icc x₁ (x₁ * log x₁) := ⟨hx₁_le_x₀, le_refl _⟩  have h_sub_div_t₀ : ∫ s in x₁..x₁ * log x₁, (s - x₁) / s = x₁ * log x₁ - x₁ - x₁ * log (log x₁) := by    have h_sub := integral_sub_div_self (by linarith : 0 < x₁) hx₁_le_x₀    rw [mul_div_cancel_left₀ _ (by linarith : x₁ ≠ 0)] at h_sub    linarith  have h_I_bound_t₀ : ∫ s in x₁..x₁ * log x₁, (∫ u in x₁..s, 1 / (log u) ^ 2) / s ≤      (1 / (log x₁) ^ 2) * (x₁ * log x₁ - x₁ - x₁ * log (log x₁)) :=    h_sub_div_t₀ ▸ integral_I_div_self_le (by linarith) ht₀_mem  have h_u_eq_t₀ := u_eq_sub_integral (by linarith) ht₀_mem  have h_pos_bound : x₁ / log x₁ - (1 / (log x₁) ^ 2) * (x₁ * log x₁ - x₁ - x₁ * log (log x₁)) > 0 := by    have h_logx₁_pos : 0 < log x₁ := Real.log_pos (by linarith)    have h_loglogx₁_pos : 0 < log (log x₁) := Real.log_pos h_logx₁_gt    have h_eq : x₁ / log x₁ - (1 / (log x₁) ^ 2) * (x₁ * log x₁ - x₁ - x₁ * log (log x₁)) =        x₁ * (1 + log (log x₁)) / (log x₁) ^ 2 := by      field_simp      ring    rw [h_eq]    positivity  linarith [h_u_eq_t₀, h_I_bound_t₀, h_pos_bound]