TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Uniqueness of the scalar Laplace transform in the exponential-growth class

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the Lebesgue-measure interfaces. Let $K \in {R, C}$ and let $f : [0, \infty) \to K$ be continuous with $∣ f (t) ∣ \leq C e^{σ t}$ for some $C \geq 0$ , $σ \in R$ and all $t \geq 0$ . If the Laplace transform vanishes on a right half-line, $\int_{0}^{\infty} e^{- λ t} f (t) d t = 0 for every real λ > σ,$ then $f (t) = 0$ for every $t \geq 0$ .

Facts & Assumptions

Given: Countable Choice; A real or complex-valued continuous $f : [0, \infty) \to K$ with $∣ f (t) ∣ \leq C e^{σ t}$ for some $C \geq 0$ , $σ \in R$ and all $t \geq 0$ , and $\int_{0}^{\infty} e^{- λ t} f (t) d t = 0$ for every real $λ > σ$ ; for $λ > σ$ the integrand is dominated by $C e^{- (λ - σ) t}$ and the integral exists as a Lebesgue integral over $[0, \infty)$ .

[F1]

If $a < b$ , $φ$ is $C^{1}$ and injective with $φ^{'} \neq 0$ on a neighbourhood of $[a, b]$ , and the continuous function $h$ is defined on an interval containing $φ ([a, b])$ , then $\int_{\min φ}^{\max φ} h = \int_{a}^{b} h (φ (t)) ∣ φ^{'} (t) ∣ d t$ (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative). This substitution is stated for Riemann integrals; on the compact intervals used below all its integrands are continuous, hence bounded and Riemann integrable, and A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral identifies those integrals with their Lebesgue integrals under Countable Choice.

[F2]

Polynomials are uniformly dense in $C ([0, 1], R)$ : for every continuous real $φ$ on $[0, 1]$ and $η > 0$ there is a polynomial $p$ with $\sup_{[0, 1]} ∣ p - φ ∣ < η$ (Polynomials are uniformly dense in $C ([0, 1], R)$ ).

[F3]

The Lebesgue integral is linear on $L^{1}$ and satisfies $∣ \int h ∣ \leq \int ∣ h ∣$ ; the integral over a measurable set is defined by restricting each real positive/negative and imaginary component, giving $\int_{E} h = \int h 1_{E}$ (The Lebesgue integral is linear on $L^{1} (μ)$ , The modulus of an integral is bounded by the integral of the modulus, The class $L^{1} (μ)$ of integrable functions, Integrable real and complex functions, and their integrals); Integral over a measurable subset alone supplies only the nonnegative convention.

Proof

technique · direct, reducing to real $f$, converting the Laplace moments into moments of a continuous function on $[0,1]$, and applying polynomial density

1.1F3algebra

It suffices to prove the theorem for real-valued $f$ : if $f$ is complex-valued, then $Re f$ and $Im f$ are continuous, satisfy the same bound $∣ Re f ∣, ∣ Im f ∣ \leq C e^{σ t}$ , and by [F3] have $\int_{0}^{\infty} e^{- λ t} Re f (t) d t = Re 0 = 0$ and likewise for $Im f$ for every real $λ > σ$ .

1.2F3algebra

Assume $f$ real. Fix $λ_{0} > \max {σ, 0}$ and put $δ : = λ_{0} - σ > 0$ and $F (t) : = e^{- λ_{0} t} f (t)$ . Then $F$ is continuous with $∣ F (t) ∣ \leq C e^{- δ t}$ for $t \geq 0$ , so $F \in L^{1} (0, \infty)$ ; moreover for every integer $k \geq 0$ the number $λ : = λ_{0} + k + 1$ exceeds $σ$ and $\int_{0}^{\infty} e^{- (k + 1) t} F (t) d t = \int_{0}^{\infty} e^{- λ t} f (t) d t = 0$ .

1.3F3algebra

Put $g (x) : = F (- \ln x)$ for $x \in (0, 1]$ and $g (0) : = 0$ . Then $g$ is continuous on $[0, 1]$ : it is continuous on $(0, 1]$ as a composition, and $∣ g (x) ∣ = ∣ F (- \ln x) ∣ \leq C x^{δ} \to 0$ as $x ↓ 0$ because $δ > 0$ , matching $g (0) = 0$ ; also $∣ g (x) ∣ \leq C x^{δ} \leq C$ on $[0, 1]$ , so $g \in L^{1} (0, 1)$ and $\int_{0}^{1} ∣ g ∣ d x \leq C$ .

2.1F1step 1.3

For $T > 0$ and $k \geq 0$ , [F1] applied on $[0, T]$ to $φ (t) = e^{- t}$ and the continuous $h (x) = x^{k} g (x)$ on $[0, 1]$ gives $\int_{e^{- T}}^{1} x^{k} g (x) d x = \int_{0}^{T} e^{- (k + 1) t} F (t) d t$ .

3.1F3step 1.2step 2.1algebra

Letting $T \to \infty$ in [step 2.1]: the right-hand side tends to $\int_{0}^{\infty} e^{- (k + 1) t} F (t) d t$ because its tail is bounded by $\int_{T}^{\infty} C e^{- (δ + k + 1) t} d t \leq C e^{- (δ + k + 1) T} / (δ + k + 1) \to 0$ ; the left-hand side tends to $\int_{0}^{1} x^{k} g (x) d x$ because the missing part satisfies $∣ \int_{0}^{e^{- T}} x^{k} g (x) d x ∣ \leq C \int_{0}^{e^{- T}} x^{δ + k} d x \leq C e^{- (k + δ + 1) T} \to 0$ ; by [step 1.2] the limits are $0$ , so $\int_{0}^{1} x^{k} g (x) d x = 0$ for every integer $k \geq 0$ .

4.1F2F3step 1.3step 3.1

Every continuous real $φ$ on $[0, 1]$ satisfies $\int_{0}^{1} φ (x) g (x) d x = 0$ : fix $η > 0$ and, by [F2], choose a polynomial $p$ with $\sup_{[0, 1]} ∣ φ - p ∣ \leq η / (1 + \int_{0}^{1} ∣ g ∣ d x)$ ; then $∣ \int_{0}^{1} (φ - p) g d x ∣ \leq \sup ∣ φ - p ∣ \int_{0}^{1} ∣ g ∣ d x < η$ by [F3], while $\int_{0}^{1} p g d x = 0$ by [step 3.1]; hence $∣ \int_{0}^{1} φ g d x ∣ < η$ for every $η > 0$ , so the integral vanishes.

5.1step 4.1algebra

The function $g$ vanishes identically on $[0, 1]$ : otherwise $g (x_{0}) \neq 0$ for some $x_{0} \in (0, 1]$ with $g (x_{0}) > 0$ (or $< 0$ ), and by continuity there is an interval $J \subseteq [0, 1]$ of positive length with $g > 0$ on $J$ (respectively $g < 0$ on $J$ ); choosing a continuous nonnegative bump $φ$ supported in $J$ with $φ (x_{0}) > 0$ gives $φ g \geq 0$ , positive at $x_{0}$ and continuous, so $\int_{0}^{1} φ g d x > 0$ (respectively $< 0$ ), contradicting [step 4.1].

6.1step 1.1step 1.3step 5.1∎

Consequently $F (t) = g (e^{- t}) = 0$ for every $t \geq 0$ , whence $f (t) = e^{λ_{0} t} F (t) = 0$ for every $t \geq 0$ in the real case; the complex case follows by applying the real case to $Re f$ and $Im f$ as in [step 1.1].

Depends on

Used by

Laplace uniqueness identifies two exponentially bounded semigroups Lemma

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Klaus-Jochen Engel and Rainer Nagel, One-Parameter Semigroups for Linear Evolution Equations, Graduate Texts in Mathematics 194 (complete author-hosted monograph) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Universitext, Springer 2011 (complete 614-page text) (standard reference, not scraped)