MeasureTheory.lintegral_Ioi_rpow_of_lt_abs

lemma lintegral_Ioi_rpow_of_lt_abs {β σ : ℝ} (hβ : 0 < β) (hσ : σ < -1) :    ∫⁻ s : ℝ in Ioi β, ENNReal.ofReal (s ^ σ) =    ENNReal.ofReal (β ^ (σ + 1) / |σ + 1|) := by  have hσ2 : σ + 1 < 0 := by linarith  rw [abs_of_neg hσ2, ← ofReal_integral_eq_lintegral_ofReal]  · rw [integral_Ioi_rpow_of_lt hσ hβ, div_neg, neg_div]  · apply integrableOn_Ioi_rpow_of_lt hσ hβ  · filter_upwards [self_mem_ae_restrict measurableSet_Ioi]    exact fun s hs ↦ Real.rpow_nonneg (lt_trans hβ hs).le σ