RS_prime.bound_deriv

theorem bound_deriv {f : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Ici 2)) {C : ℝ}    (hC : ∀ x ∈ Set.Ici 2, |f x| ≤ C / x ∧ |deriv f x| ≤ C / x ^ 2) :    ∀ᵐ (a : ℝ) ∂volume.restrict (Set.Ioi 2), ‖deriv (fun t ↦ f t / log t) a‖ ≤    C * (1 / (a ^ 2 * log a) + 1 / (a ^ 2 * log a ^ 2)) := by  filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha  calc  _ = ‖deriv f a / log a - f a / (a * log a ^ 2)‖ := by    congr    rw [deriv_fun_div, deriv_log]    · field_simp    · exact hf.differentiableAt (mem_nhds_iff.2 ⟨Set.Ioi 2, Set.Ioi_subset_Ici_self,        ⟨isOpen_Ioi, ha⟩⟩)    · exact differentiableAt_log_iff.2 (by grind)    · simp_all; grind  _ ≤ ‖deriv f a‖ / ‖log a‖ + ‖f a‖ / ‖a * log a ^ 2‖ := by rw [← norm_div, ← norm_div]; bound  _ = |deriv f a| / ‖log a‖ + |f a| / ‖a * log a ^ 2‖ := by simp  _ ≤ C / a ^ 2 / ‖log a‖ + C / a / ‖a * log a ^ 2‖ := by    gcongr    exacts [(hC a (Set.Ioi_subset_Ici_self ha)).2, (hC a (Set.Ioi_subset_Ici_self ha)).1]  _ = C / a ^ 2 / log a + C / a / (a * log a ^ 2) := by    congr <;> rw [norm_of_nonneg]    · exact log_nonneg (by grind)    · exact mul_nonneg (by grind) (pow_nonneg (log_nonneg (by grind)) 2)  _ = _ := by field_simp