RS_prime.integrableOn_deriv_inv

theorem integrableOn_deriv_inv : IntegrableOn (fun y ↦ - ((θ y - y) / y ^ 2)) (Set.Ioi 2) volume ∧    ∀ x ≥ 2, IntervalIntegrable (fun t ↦ -(t ^ 2)⁻¹) volume 2 x := by  obtain ⟨C, hC⟩ := pnt  refine ⟨Integrable.mono' (g := fun t => C / (t * log t ^ 2)) ?_ ?_ ?_, fun x hx =>    ContinuousOn.intervalIntegrable (Set.uIcc_of_le hx ▸ by fun_prop (disch := simp_all; grind))⟩  · simp only [fun t => div_eq_mul_one_div C (t * Real.log t ^ 2)]    exact (ioiIntegrable_inv_log_pow (by grind) (by grind)).const_mul C  · exact ((theta_mono.measurable.sub (by fun_prop)).div (by fun_prop)).neg.aestronglyMeasurable  · filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha    calc    _ = |(θ a - a)| / ‖a ^ 2‖ := by simp    _ ≤ C * a / Real.log a ^ 2 / a ^ 2 := by grw [hC.2 a ha.le]; simp    _ = _ := by field_simp