LemmaStatement: 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.

The variation-of-constants integral is continuous for integrable forcing

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for Lebesgue time integration. Let $(T (t))_{t \geq 0}$ be a strongly continuous semigroup on a Banach space $X$ with constants $M \geq 1$ , $ω \in R$ and $∥ T (t) ∥ \leq M e^{ω t}$ (Exponential bound for a C0-semigroup). Let $T_{0} > 0$ and let $f : (0, T_{0}) \to X$ be Bochner integrable with $\int_{0}^{T_{0}} ∥ f (s) ∥ d s < \infty$ (Bochner-integrable function). Then $u_{f} (t) : = \int_{0}^{t} T (t - s) f (s) d s (0 \leq t \leq T_{0})$ is a well-defined element of $X$ , the map $t \mapsto u_{f} (t)$ is continuous on $[0, T_{0}]$ , and $∥ u_{f} (t) ∥ \leq M_{T_{0}} e^{ω t} \int_{0}^{t} ∥ f (s) ∥ d s$ for a constant $M_{T_{0}}$ depending only on $M, ω, T_{0}$ and the local bound of $∥ T ∥$ on $[0, T_{0}]$ .

Facts & Assumptions

Given: Countable Choice; A strongly continuous semigroup $(T (t))_{t \geq 0}$ on a Banach space $X$ with $∥ T (t) ∥ \leq M e^{ω t}$ for some $M \geq 1$ , $ω \in R$ (Exponential bound for a C0-semigroup); $T_{0} > 0$ ; a Bochner integrable $f : (0, T_{0}) \to X$ with $\int_{0}^{T_{0}} ∥ f (s) ∥ d s < \infty$ ; and $u_{f} (t) : = \int_{0}^{t} T (t - s) f (s) d s$ .

[F1]

The exponential bound makes $K : = \sup_{0 \leq r \leq T_{0}} ∥ T (r) ∥$ finite, since $∥ T (r) ∥ \leq M e^{ω r} \leq M e^{\max (ω, 0) T_{0}}$ . [thm-exponential-bound-for-a-c-zero-semigroup]

[F2]

Bochner integrability of $f$ supplies integrable simple functions $g$ with $\int (0, T_{0}) ∥ f - g ∥$ arbitrarily small and a strong-measurability approximation (Bochner-integrable function, Strongly measurable Banach-valued function); a strongly measurable $h$ with $\int ∥ h ∥ < \infty$ is Bochner integrable (Bochner integrability criterion).

[F3]

Linearity of the Bochner integral and the norm inequality $∥ \int_{E} h ∥ \leq \int_{E} ∥ h ∥$ (Linearity of the Bochner integral, Bochner integral norm inequality, Bochner-integrable function).

[F4]

Absolute continuity of the scalar integral: for every $ε > 0$ there is $δ > 0$ with $\int_{E} ∥ f ∥ < ε$ whenever $λ (E) < δ$ (Absolute continuity of the integral).

[F5]

The orbit map of every vector is continuous on $[0, \infty)$ and $T (h) \to I$ strongly: $T (h) x \to x$ for every $x$ (Strongly continuous semigroup).

Proof

technique · direct: well-definedness from the Bochner criterion, then a uniform estimate $\int\|(T(h)-I)f\|\to0$ obtained from a single simple approximation, and a splitting of the increment

1.1F1F2F3F5

Fix $t \in [0, T_{0}]$ . For each measurable simple approximation $g_{n} = \sum_{j} x_{n j} 1_{E_{n j}}$ to $f$ , the map $s \mapsto T (t - s) g_{n} (s)$ is strongly measurable: for each of its finitely many values $x_{n j}$ , approximate the continuous curve $s \mapsto T (t - s) x_{n j}$ uniformly by step functions on equal partitions of $[0, t]$ , then multiply by $1_{E_{n j}}$ . Choose a partition size by its least integer giving error below $1 / n$ on all finitely many curves. The resulting measurable simple function approximates $T (t - s) g_{n} (s)$ uniformly within $1 / n$ . As $g_{n} (s) \to f (s)$ off a null set and $∥ T (t - s) ∥ \leq K$ , these approximants converge pointwise there to $T (t - s) f (s)$ . Its norm is bounded by $K ∥ f (s) ∥$ , so [F2] gives Bochner integrability and [F3] gives $∥ u_{f} (t) ∥ \leq M e^{\max (- ω, 0) T_{0}} e^{ω t} \int_{0}^{t} ∥ f (s) ∥ d s$ .

1.2F1F2F5

Claim: $ρ (h) : = \int_{0}^{T_{0}} ∥ (T (h) - I) f (s) ∥ d s \to 0$ as $h ↓ 0$ . Given $ε > 0$ , choose an integrable simple function $g = \sum_{j = 1}^{m} x_{j} 1_{E_{j}}$ with $\int_{0}^{T_{0}} ∥ f - g ∥ < ε / (2 (K + 1))$ by [F2]; then $ρ (h) \leq (K + 1) \int ∥ f - g ∥ + \sum_{j} λ (E_{j}) ∥ (T (h) - I) x_{j} ∥$ , and the finite sum tends to $0$ as $h ↓ 0$ because $T (h) x_{j} \to x_{j}$ for each $j$ by [F5]. Hence ${lim sup}_{h} ρ (h) \leq ε / 2 < ε$ , and $ε$ was arbitrary.

2.1F3step 1.1

Increment splitting: for $0 \leq t < t + h \leq T_{0}$ , linearity [F3] and the semigroup law give $u_{f} (t + h) - u_{f} (t) = \int_{0}^{t + h} T (t + h - s) f (s) d s - \int_{0}^{t} T (t - s) f (s) d s = \int_{t}^{t + h} T (t + h - s) f (s) d s + \int_{0}^{t} T (t - s) (T (h) - I) f (s) d s$ , where in the last term $T (t - s + h) = T (t - s) T (h)$ .

3.1F1F3F4step 1.2step 2.1

Taking norms in [step 2.1] and using $K$ from [F1] and the norm inequality [F3]: $∥ u_{f} (t + h) - u_{f} (t) ∥ \leq K \int_{t}^{t + h} ∥ f (s) ∥ d s + K ρ (h) \to 0$ as $h ↓ 0$ , the first term by absolute continuity [F4] and the second by [step 1.2]. The backward increment is bounded by $K \int_{t - h}^{t} ∥ f ∥ + K ρ (h)$ by the same splitting with $t - h$ in place of $t$ , hence also tends to $0$ .

4.1F1F3F4step 3.1

Continuity at the endpoints: $∥ u_{f} (h) - u_{f} (0) ∥ \leq K \int_{0}^{h} ∥ f ∥ \to 0$ by [F3], [F4], and at $t = T_{0}$ the backward bound of [step 3.1] applies; hence $t \mapsto u_{f} (t)$ is continuous on the closed interval $[0, T_{0}]$ , and the estimate of [step 1.1] is the stated bound with $M_{T_{0}} : = M e^{\max (- ω, 0) T_{0}}$ .

5.1step 1.1step 1.2step 3.1step 4.1∎

The claims of the statement follow: $u_{f}$ is well defined, continuous on $[0, T_{0}]$ , and bounded by $M_{T_{0}} e^{ω t} \int_{0}^{t} ∥ f ∥$ ; no compactness of the range of $f$ and no choice beyond the declared Bochner framework was used.

Depends on

Used by

Dependency tree · two levels

36 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)
Mathew A. Johnson, Math 951 Lecture Notes, Chapter 6: Introduction to Semigroup Methods, University of Kansas (complete 37-page chapter) (standard reference, not scraped)