push_cast
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1)) * cexp (2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)