Theorem: second_fourier_integrable_aux2 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun u => cexp ((1 - ↑σ' - ↑t * I) * ↑u)) (Ioi (-x.log)) volume
Tactic:
refine (integrable_norm_iff (Measurable.aestronglyMeasurable <| by fun_prop)).mp ?_
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ Integrable (fun a => ‖cexp ((1 - ↑σ' - ↑t * I) * ↑a)‖) (volume.restrict (Ioi (-x.log)))

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

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ IntegrableOn (fun a => rexp (-(σ' - 1) * a)) (Ioi (-x.log)) volume
Tactic:
apply exp_neg_integrableOn_Ioi
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ 0 < σ' - 1

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ 0 < σ' - 1
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hσ : 1 < σ'
⊢ Measurable fun u => cexp ((1 - ↑σ' - ↑t * I) * ↑u)
Tactic:
fun_prop
State after:
no goals

State before:
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)))
Tactic:
simpa [Complex.abs_exp]
State after:
no goals