Fourier–Laplace transform

DefinitionFourier–Laplace transform#✓fully proved

For \(f : \mathbb{R} \to \mathbb{C}\) and \(z \in \mathbb{C}\), the Fourier–Laplace transform of \(f\) at \(z\) is the Lebesgue integral \(\int_{\mathbb{R}} f(x) \, e^{-2\pi i x z} \, dx\), taken to be \(0\) when the integrand is not integrable.

noncomputable def fourierLaplace (f : ℝ → ℂ) (z : ℂ) : ℂ :=
  ∫ x : ℝ, f x * Complex.exp (-2 * (Real.pi : ℂ) * Complex.I * (x : ℂ) * z)

Used by 3

Used byThe Fourier–Laplace transform of an integrable compactly supported function is entire · Fourier–Laplace transform on the real axis · Derivative of the Fourier–Laplace transform

TheoremFourier–Laplace transform on the real axis#✓fully proved

For every \(f : \mathbb{R} \to \mathbb{C}\) and every real \(r\), the Fourier–Laplace transform of \(f\) at the complex number \(r\), namely \(\int_{\mathbb{R}} f(x) \, e^{-2\pi i x r} \, dx\), equals the Fourier transform of \(f\) at \(r\) with the \(2\pi\) normalization, \(\hat f(r) = \int_{\mathbb{R}} e^{-2\pi i x r} f(x) \, dx\).

theorem fourierLaplace_ofReal (f : ℝ → ℂ) (r : ℝ) :
    fourierLaplace f (r : ℂ) = Fourier.fourierIntegral Real.fourierChar volume f r

Uses 1

Statement usesFourier–Laplace transform

TheoremDerivative of the Fourier–Laplace transform#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{C}\) be integrable with compact support, and let \(F(z) = \int_{\mathbb{R}} f(x) \, e^{-2\pi i x z} \, dx\) be its Fourier–Laplace transform. Then at every \(z \in \mathbb{C}\), \(F\) is complex differentiable with derivative \(F'(z) = \int_{\mathbb{R}} f(x) \, (-2\pi i x) \, e^{-2\pi i x z} \, dx\).

theorem hasDerivAt_fourierLaplace {f : ℝ → ℂ} (hf : Integrable f)
    (hfc : HasCompactSupport f) (z : ℂ) :
    HasDerivAt (fourierLaplace f)
      (∫ x : ℝ, f x * ((-2 * (Real.pi : ℂ) * Complex.I * (x : ℂ)) *
        Complex.exp (-2 * (Real.pi : ℂ) * Complex.I * (x : ℂ) * z))) z

Uses 1 · Used by 1

Statement usesFourier–Laplace transform

Used byThe Fourier–Laplace transform of an integrable compactly supported function is entire

TheoremThe Fourier–Laplace transform of an integrable compactly supported function is entire#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{C}\) be integrable with compact support. Then its Fourier–Laplace transform \(z \mapsto \int_{\mathbb{R}} f(x) \, e^{-2\pi i x z} \, dx\) is complex differentiable at every \(z \in \mathbb{C}\), that is, it is entire.

theorem differentiable_fourierLaplace {f : ℝ → ℂ} (hf : Integrable f)
    (hfc : HasCompactSupport f) : Differentiable ℂ (fourierLaplace f)

Uses 2

Statement usesFourier–Laplace transform

Proof usesDerivative of the Fourier–Laplace transform

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.