Source indexedtheorem · leanprover/lean4:v4.32.0

laplaceTransformBilateral_eq_fourier

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:100 to 123

Source documentation

On a vertical line, the bilateral Laplace transform is the Fourier transform of the exponentially weighted function.

Exact Lean statement

theorem laplaceTransformBilateral_eq_fourier (f : ℝ → E) (s : ℂ) :
    laplaceTransformBilateral f s =
      𝓕 (fun x : ℝ => Complex.exp (-(s.re : ℂ) * (x : ℂ)) • f x) (s.im / (2 * π))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem laplaceTransformBilateral_eq_fourier (f : ℝ → E) (s : ℂ) :    laplaceTransformBilateral f s =      𝓕 (fun x : ℝ => Complex.exp (-(s.re : ℂ) * (x : ℂ)) • f x) (s.im / (2 * π)) := by  calc    laplaceTransformBilateral f s      = ∫ x : ℝ, Complex.exp (-(s.im : ℂ) * (x : ℂ) * I) •          (Complex.exp (-(s.re : ℂ) * (x : ℂ)) • f x) := by        unfold laplaceTransformBilateral        congr        ext x        conv => lhs; rw [← re_add_im s]        rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]        norm_cast        push_cast        ring_nf    _ = 𝓕 (fun x : ℝ => Complex.exp (-(s.re : ℂ) * (x : ℂ)) • f x) (s.im / (2 * π)) := by      rw [Real.fourier_eq']      congr      ext x      congr 1      have h2pi : (2 * (π : ℝ) : ℂ) ≠ 0 := by norm_num [Real.pi_ne_zero]      rw [Real.inner_apply]      push_cast      field_simp [h2pi]