exact second_fourier_integrable_aux1 hcont hsupp hσ
case hf
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 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)

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 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
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 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)