RS_prime.ioiIntegrable_inv_log_pow

theorem ioiIntegrable_inv_log_pow {n : ℕ} (hn : 1 < n) {x : ℝ} (hx : 1 < x) :    IntegrableOn (fun t ↦ 1 / (t * Real.log t ^ n)) (Set.Ioi x) volume := by  refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (log x ^ (1 - (n : ℝ)) / (n - 1)) x    (fun k => ?_) tendsto_natCast_atTop_atTop ?_  · simpa using intervalIntegrable_inv_log_pow 1 n hx k  · have : 0 < (n : ℝ) - 1 := by linarith [(one_lt_cast (α := ℝ)).2 hn]    refine Tendsto.congr' (f₁ := fun i : ℕ => (log i : ℝ) ^ (1 - (n : ℝ)) / (1 - (n : ℝ)) -      (log x) ^ (1 - (n : ℝ)) / (1 - (n : ℝ))) ?_ ?_    · have := tendsto_def.1 tendsto_natCast_atTop_atTop (Set.Ici x) (Ici_mem_atTop x)      filter_upwards [this] with i hi      refine (intervalIntegral.integral_eq_sub_of_hasDerivAt        (f := fun r => log r ^ (1 - (n : ℝ)) / (1 - (n : ℝ))) (fun z hz => ?_) ?_).symm      · simp_all only [preimage_Ici, Set.mem_Ici, ceil_le, Set.uIcc_of_le, Set.mem_Icc]        have := Real.log_pos (by linarith)        rw [norm_of_nonneg <| one_div_nonneg.2 (mul_nonneg (by grind) (pow_nonneg this.le n))]        refine (((hasDerivAt_log (by grind)).rpow_const (by grind)).div_const _).congr_deriv ?_        have : 1 - (n : ℝ) ≠ 0 := by linarith        simp [field]      · apply IntervalIntegrable.norm        simpa using (intervalIntegrable_iff_integrableOn_Ioc_of_le hi).2          (intervalIntegrable_inv_log_pow 1 n hx i)    · suffices h : Tendsto (fun i : ℕ ↦ Real.log i ^ (1 - (n : ℝ)) / (1 - n)) atTop (𝓝 0) from by        have : (log x ^ (1 - (n : ℝ)) / (n - 1)) = 0 - (log x ^ (1 - (n : ℝ)) / (1 - n)) := by grind        exact this ▸ h.sub_const (log x ^ (1 - (n : ℝ)) / (1 - n))      simpa using (((tendsto_rpow_neg_atTop this).comp tendsto_log_atTop).comp        tendsto_natCast_atTop_atTop).div_const (1 - (n : ℝ))