simp_rw [fun (a x : ℝ) ↦ (by ring : -(x * a) = -a * x), integrableOn_Ici_iff_integrableOn_Ioi]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => rexp (-(x * (σ' - 1)))) (Ici (-x.log)) volume
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun x => rexp (-(σ' - 1) * x)) (Ioi (-x.log)) volume