Source indexedtheorem · leanprover/lean4:v4.32.0

laplace_deriv_integrand_integrable

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:230 to 242

Source documentation

The derivative integrand -(y)·φ(y)·e^{-σy} is integrable for σ in the strip.

Exact Lean statement

theorem laplace_deriv_integrand_integrable {φ : ℝ → ℂ} {b σ : ℝ} (hφc : Continuous φ)
    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]
      fun x ↦ Real.exp (-(1/2+b)*|x|))
    (hσtop : -(1+b) < σ) (hσbot : σ < b) :
    Integrable (fun y : ℝ ↦ (-(y:ℂ) * φ y) * Complex.exp (-(σ:ℂ)*y))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem laplace_deriv_integrand_integrable {φ : ℝ → ℂ} {b σ : ℝ} (hφc : Continuous φ)    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b)*|x|))    (hσtop : -(1+b) < σ) (hσbot : σ < b) :    Integrable (fun y : ℝ ↦ (-(y:ℂ) * φ y) * Complex.exp (-(σ:ℂ)*y)) := by  set b' := (max σ (-1-σ) + b)/2 with hb'def  have hmax : max σ (-1-σ) < b := max_lt hσbot (by linarith)  have hMle : max σ (-1-σ) < b' := by rw [hb'def]; linarith  have hb'bot : σ < b' := lt_of_le_of_lt (le_max_left _ _) hMle  have hb'top : -(1+b') < σ := by    have := lt_of_le_of_lt (le_max_right σ (-1-σ)) hMle; linarith  exact laplace_integrand_integrable (φ := fun y ↦ -(y:ℂ) * φ y) (by fun_prop)    (neg_id_mul_decay (by rw [hb'def]; linarith) hφ_decay) hb'top hb'bot