Source indexedtheorem · leanprover/lean4:v4.32.0

laplaceInvLineTrunc_tendsto_laplaceTransformBilateral_eq

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2346 to 2371

Source documentation

Principal-value Laplace inversion reduced to the corresponding truncated Fourier convergence theorem for the exponentially weighted source.

Exact Lean statement

theorem laplaceInvLineTrunc_tendsto_laplaceTransformBilateral_eq
    (sigma : ℝ) (f : ℝ → E) {x : ℝ}
    (hlim : Filter.Tendsto
      (fun T : ℝ =>
        fourierInvTrunc
          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y)) x T)
      Filter.atTop
      (nhds (Complex.exp (-((sigma : ℂ) * (x : ℂ))) • f x))) :
    Filter.Tendsto
      (fun T : ℝ => laplaceInvLineTrunc sigma (laplaceTransformBilateral f) x T)
      Filter.atTop (nhds (f x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem laplaceInvLineTrunc_tendsto_laplaceTransformBilateral_eq    (sigma : ℝ) (f : ℝ → E) {x : ℝ}    (hlim : Filter.Tendsto      (fun T : ℝ =>        fourierInvTrunc          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y)) x T)      Filter.atTop      (nhds (Complex.exp (-((sigma : ℂ) * (x : ℂ))) • f x))) :    Filter.Tendsto      (fun T : ℝ => laplaceInvLineTrunc sigma (laplaceTransformBilateral f) x T)      Filter.atTop (nhds (f x)) := by  let g : ℝ → E := fun y => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y  have hlim' : Filter.Tendsto (fun T : ℝ => fourierInvTrunc (𝓕 g) x T)      Filter.atTop (nhds (g x)) := by    simpa [g] using hlim  have hscaled : Filter.Tendsto      (fun T : ℝ =>        Complex.exp ((sigma : ℂ) * (x : ℂ)) • fourierInvTrunc (𝓕 g) x T)      Filter.atTop (nhds (Complex.exp ((sigma : ℂ) * (x : ℂ)) • g x)) :=    hlim'.const_smul (Complex.exp ((sigma : ℂ) * (x : ℂ)))  have htarget : Complex.exp ((sigma : ℂ) * (x : ℂ)) • g x = f x := by    simp [g, ← smul_assoc, ← Complex.exp_add]  rw [htarget] at hscaled  refine hscaled.congr' ?_  filter_upwards with T  exact (laplaceInvLineTrunc_laplaceTransformBilateral_eq_fourierInvTrunc sigma f x T).symm