simpa [Complex.abs_exp]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
this : IntegrableOn (fun a => rexp (-(σ' - 1) * a)) (Ioi (-x.log)) ?m.446246
⊢ Integrable (fun a => ‖cexp ((1 - ↑σ' - ↑t * I) * ↑a)‖) (volume.restrict (Ioi (-x.log)))
no goals