let f1 : ℝ → ENNReal := fun a1 ↦ ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
f1 : ℝ → ENNReal := fun a1 => ↑‖cexp (-(↑a1 * (↑σ' - 1)))‖₊
⊢ HasFiniteIntegral
    (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • ↑(𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π)))))) • ψ a) ν