Theorem: vertical_integrable_Smooth1 (PrimeNumberTheoremAnd/MediumPNT.lean)

State before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
sorry
State after:
no goals