RS_prime.integrableOn_deriv

theorem integrableOn_deriv {f : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Ici 2)) {C : ℝ}    (hC : ∀ x ∈ Set.Ici 2, |f x| ≤ C / x ∧ |deriv f x| ≤ C / x ^ 2) :    IntegrableOn (fun y ↦ (θ y - y) * deriv (fun t ↦ f t / log t) y) (Set.Ioi 2) volume    ∧ ∀ x ≥ 2, IntervalIntegrable (fun t ↦ deriv (fun s ↦ f s / Real.log s) t) volume 2 x := by  obtain ⟨A, hA⟩ := pnt  refine ⟨Integrable.mono' (g := fun t => (A * C) * (1 / (t * log t ^ 3) + 1 / (t * log t ^ 4)))    ?_ ?_ ?_, fun x hx => ?_⟩  · refine ((ioiIntegrable_inv_log_pow ?_ ?_).add (ioiIntegrable_inv_log_pow ?_ ?_)).const_mul      (A * C) <;> linarith  · exact (theta_mono.measurable.aestronglyMeasurable.sub (by fun_prop)).mul      (aestronglyMeasurable_deriv _ _)  · filter_upwards [bound_deriv hf hC, ae_restrict_mem measurableSet_Ioi] with a ha ho    calc    _ = |(θ a - a)| * ‖deriv (fun t ↦ f t / log t) a‖ := by simp    _ ≤ A * a / log a ^ 2 * (C * (1 / (a ^ 2 * log a) + 1 / (a ^ 2 * log a ^ 2))) := by      gcongr      · exact div_nonneg (mul_nonneg hA.1 (by grind)) (pow_nonneg (log_nonneg (by grind)) 2)      · exact hA.2 a (Set.mem_Ioi.1 ho).le    _ = _ := by field_simp  · refine (intervalIntegrable_iff_integrableOn_Ioc_of_le hx).2 (Integrable.mono'      (Integrable.const_mul (Integrable.add ?_ ?_) C) (aestronglyMeasurable_deriv _ _)      (ae_restrict_of_ae_restrict_of_subset Set.Ioc_subset_Ioi_self (bound_deriv hf hC)))    · simpa using! intervalIntegrable_inv_log_pow 2 1 (by linarith : 1 < (2 : ℝ)) x    · simpa using! intervalIntegrable_inv_log_pow 2 2 (by linarith : 1 < (2 : ℝ)) x