Source indexedtheorem · leanprover/lean4:v4.32.0

laplaceIntegralCpowTrunc_tendsto_of_fourierInvTrunc

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2404 to 2427

Source documentation

Principal-value Laplace inversion in the multiplication x^s form, reduced to truncated Fourier convergence for the exponentially weighted source.

Exact Lean statement

theorem laplaceIntegralCpowTrunc_tendsto_of_fourierInvTrunc
    (sigma : ℝ) (f : ℝ → ℂ) {x : ℝ} (hx : 0 < x)
    (hlim : Filter.Tendsto
      (fun T : ℝ =>
        fourierInvTrunc
          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) * f y))
          (Real.log x) T)
      Filter.atTop
      (nhds (Complex.exp (-((sigma : ℂ) * (Real.log x : ℂ))) * f (Real.log x)))) :
    Filter.Tendsto (fun T : ℝ => laplaceIntegralCpowTrunc f sigma x T)
      Filter.atTop (nhds (f (Real.log x)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem laplaceIntegralCpowTrunc_tendsto_of_fourierInvTrunc    (sigma : ℝ) (f : ℝ → ℂ) {x : ℝ} (hx : 0 < x)    (hlim : Filter.Tendsto      (fun T : ℝ =>        fourierInvTrunc          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) * f y))          (Real.log x) T)      Filter.atTop      (nhds (Complex.exp (-((sigma : ℂ) * (Real.log x : ℂ))) * f (Real.log x)))) :    Filter.Tendsto (fun T : ℝ => laplaceIntegralCpowTrunc f sigma x T)      Filter.atTop (nhds (f (Real.log x))) := by  have hlim' : Filter.Tendsto      (fun T : ℝ =>        fourierInvTrunc          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y))          (Real.log x) T)      Filter.atTop      (nhds (Complex.exp (-((sigma : ℂ) * (Real.log x : ℂ))) • f (Real.log x))) := by    simpa [smul_eq_mul] using hlim  have hcore := laplaceInvLineTrunc_tendsto_laplaceTransformBilateral_eq    (E := ℂ) sigma f (x := Real.log x) hlim'  refine hcore.congr' ?_  filter_upwards with T  exact (laplaceIntegralCpowTrunc_eq_laplaceInvLineTrunc sigma f hx T).symm