Laplace transform

DefinitionConvergence of the Laplace transform#✓fully proved

Let \(E\) be a complex normed space, \(f : \mathbb{R} \to E\) and \(s \in \mathbb{C}\). The Laplace transform of \(f\) converges at \(s\) when the function \(t \mapsto e^{-st} f(t)\) is integrable on \((0, \infty)\) with respect to Lebesgue measure.

Integrability here is absolute (Bochner) integrability, so conditionally convergent Laplace integrals are not covered.

def LaplaceConvergent (f : ℝ → E) (s : ℂ) : Prop :=
  IntegrableOn (fun t : ℝ => Complex.exp (-s * (t : ℂ)) • f t) (Set.Ioi 0)

Sources

• ATLAS NumberTheoryI Definition 16.9 introduces the Laplace transform for real-valued functions; here functions are complex-valued (or valued in a complex normed space), and the source's real-valued case is covered by coercion.

Used by 10

Used byHolomorphy of the Laplace transform under exponential growth · Holomorphy of the Laplace transform under an exponential bound · Laplace transform with a given value · Convergence of the Laplace transform under exponential growth · Convergence of the Laplace transform under an exponential bound · Newman's Tauberian theorem · Laplace transform of the normalized Chebyshev error · Convergence of the Laplace transform of \(\theta(e^t)\) · Mertens' theorem in arithmetic progressions · Prime number theorem for Chebyshev's function in a reduced residue class

DefinitionThe one-sided Laplace transform#✓fully proved

Let \(E\) be a complex normed space, \(f : \mathbb{R} \to E\) and \(s \in \mathbb{C}\). The Laplace transform of \(f\) at \(s\) is the Bochner integral \(\int_{(0, \infty)} e^{-st} f(t)\,dt \in E\).

It is defined for every \(s\), with no convergence hypothesis: where \(t \mapsto e^{-st} f(t)\) is not integrable on \((0, \infty)\), or when \(E\) is not complete, the integral is \(0\) by convention. Convergence of the Laplace transform is a separate notion.

noncomputable def laplace (f : ℝ → E) (s : ℂ) : E :=
  ∫ t : ℝ in Set.Ioi 0, Complex.exp (-s * (t : ℂ)) • f t

Used by 10

Used byHolomorphy of the Laplace transform under exponential growth · Holomorphy of the Laplace transform under an exponential bound · Laplace transform with a given value · Newman's Tauberian theorem · Holomorphy of the Laplace transform of \(\theta(e^t)\) · Laplace transform of the normalized Chebyshev error · Convergence of the Laplace transform of \(\theta(e^t)\) · Laplace transform of \(\theta(e^t)\) · Mertens' theorem in arithmetic progressions · Prime number theorem for Chebyshev's function in a reduced residue class

DefinitionLaplace transform with a given value#✓fully proved

Let \(E\) be a complex normed space, \(f : \mathbb{R} \to E\), \(s \in \mathbb{C}\) and \(v \in E\). Then \(f\) has Laplace transform \(v\) at \(s\) when the Laplace transform of \(f\) converges at \(s\), that is, \(t \mapsto e^{-st} f(t)\) is integrable on \((0, \infty)\), and the Bochner integral \(\int_{(0, \infty)} e^{-st} f(t)\,dt\) equals \(v\); as usual this integral is taken to be \(0\) when \(E\) is not complete.

def HasLaplace (f : ℝ → E) (s : ℂ) (v : E) : Prop :=
  LaplaceConvergent f s ∧ laplace f s = v

Uses 2 · Used by 5

Statement usesConvergence of the Laplace transform · The one-sided Laplace transform

Used byNewman's Tauberian theorem · Laplace transform of the normalized Chebyshev error · Convergence of the Laplace transform of \(\theta(e^t)\) · Mertens' theorem in arithmetic progressions · Prime number theorem for Chebyshev's function in a reduced residue class

TheoremConvergence of the Laplace transform under an exponential bound#✓fully proved

Let \(E\) be a complex normed space, \(f : \mathbb{R} \to E\) almost everywhere strongly measurable on \((0, \infty)\), and \(a, C \in \mathbb{R}\) with \(C \ge 0\) such that \(\|f(t)\| \le C e^{a t}\) for all \(t \ge 0\). Then for every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > a\) the Laplace transform of \(f\) converges at \(s\), that is, \(t \mapsto e^{-st} f(t)\) is integrable on \((0, \infty)\).

theorem laplaceConvergent_of_norm_le_exp
    (f : ℝ → E) (a C : ℝ)
    (hf : AEStronglyMeasurable f (volume.restrict (Set.Ioi 0)))
    (hC : 0 ≤ C)
    (hbound : ∀ t : ℝ, 0 ≤ t → ‖f t‖ ≤ C * Real.exp (a * t))
    {s : ℂ} (hs : a < s.re) :
    LaplaceConvergent f s

Uses 1 · Used by 4

Statement usesConvergence of the Laplace transform

Used byHolomorphy of the Laplace transform under an exponential bound · Convergence of the Laplace transform of \(\theta(e^t)\) · Mertens' theorem in arithmetic progressions · Prime number theorem for Chebyshev's function in a reduced residue class

TheoremConvergence of the Laplace transform under exponential growth#✓fully proved

Let \(E\) be a complex normed space, \(a \in \mathbb{R}\), and \(f : \mathbb{R} \to E\) locally integrable on \([0, \infty)\) with \(\|f(t)\| = O(e^{a t})\) as \(t \to \infty\). Then for every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > a\) the Laplace transform of \(f\) converges at \(s\), that is, \(t \mapsto e^{-st} f(t)\) is integrable on \((0, \infty)\).

Local integrability on \([0, \infty)\), not only on \((0, \infty)\), is needed: \(f(t) = 1/t\) is continuous on \((0, \infty)\) and bounded at infinity, but not integrable near \(0\).

theorem laplaceConvergent_of_isBigO_exp
    (f : ℝ → E) (a : ℝ)
    (hloc : LocallyIntegrableOn f (Set.Ici 0))
    (ho : f =O[Filter.atTop] (fun t : ℝ => Real.exp (a * t)))
    {s : ℂ} (hs : a < s.re) :
    LaplaceConvergent f s

Sources

• ATLAS NumberTheoryI N320 (Sutherland, 18.785 Number Theory I, Lecture 16); a corrected, strengthened-premise formalization of the intended convergence claim, since the source's piecewise continuity on the open ray does not give integrability near 0. This is not a literal proof of the under-specified source wording.

Uses 1 · Used by 1

Statement usesConvergence of the Laplace transform

Used byHolomorphy of the Laplace transform under exponential growth

TheoremHolomorphy of the Laplace transform under an exponential bound#✓fully proved

Let \(E\) be a complex Banach space, \(f : \mathbb{R} \to E\) almost everywhere strongly measurable on \((0, \infty)\), and \(a, C \in \mathbb{R}\) with \(C \ge 0\) such that \(\|f(t)\| \le C e^{a t}\) for all \(t \ge 0\). Then the Laplace transform \(s \mapsto \int_{(0, \infty)} e^{-st} f(t)\,dt\) is complex differentiable at every point of the half-plane \(\{s \in \mathbb{C} : \operatorname{Re} s > a\}\).

theorem differentiableOn_laplace_of_norm_le_exp
    (f : ℝ → E) (a C : ℝ)
    (hf : AEStronglyMeasurable f (volume.restrict (Set.Ioi 0)))
    (hC : 0 ≤ C)
    (hbound : ∀ t : ℝ, 0 ≤ t → ‖f t‖ ≤ C * Real.exp (a * t))
    [CompleteSpace E] :
    DifferentiableOn ℂ (laplace f) {s | a < s.re}

Uses 3 · Used by 2

Statement usesThe one-sided Laplace transform

Proof usesConvergence of the Laplace transform · Convergence of the Laplace transform under an exponential bound

Used byNewman's Tauberian theorem · Holomorphy of the Laplace transform of \(\theta(e^t)\)

TheoremHolomorphy of the Laplace transform under exponential growth#✓fully proved

Let \(E\) be a complex Banach space, \(a \in \mathbb{R}\), and \(f : \mathbb{R} \to E\) locally integrable on \([0, \infty)\) with \(\|f(t)\| = O(e^{a t})\) as \(t \to \infty\). Then the Laplace transform \(s \mapsto \int_{(0, \infty)} e^{-st} f(t)\,dt\) is complex differentiable at every point of the half-plane \(\{s \in \mathbb{C} : \operatorname{Re} s > a\}\).

Local integrability on \([0, \infty)\), not only on \((0, \infty)\), is what makes the Laplace integral converge on this half-plane: \(f(t) = 1/t\) is continuous on \((0, \infty)\) and bounded at infinity, but not integrable near \(0\), so its Laplace integral diverges for every \(s\).

theorem differentiableOn_laplace_of_isBigO_exp
    (f : ℝ → E) (a : ℝ)
    (hf : LocallyIntegrableOn f (Set.Ici 0))
    (hO : f =O[Filter.atTop] (fun t : ℝ => Real.exp (a * t)))
    [CompleteSpace E] :
    DifferentiableOn ℂ (laplace f) {s | a < s.re}

Sources

• ATLAS NumberTheoryI N320 (Sutherland, 18.785 Number Theory I, Lecture 16); a corrected, strengthened-premise formalization of the intended holomorphy claim, since the source's piecewise continuity on the open ray does not give integrability near 0. This is not a literal proof of the under-specified source wording.

Uses 3

Statement usesThe one-sided Laplace transform

Proof usesConvergence of the Laplace transform · Convergence of the Laplace transform under exponential growth

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.