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 right-translation semigroup on Lp has the weak derivative as generator
Example
Assume Countable Choice (The Axiom of Countable Choice ()). Let and (The space as the quotient by null functions). For and define (the right translation, represented on the a.e. class by Translation of a function on ). Then is a strongly continuous semigroup of isometries on (each has norm ), and its generator is the derivative being the weak derivative (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms). Moreover for every .
Verification
Given: Countable Choice; ; ; for ; ; for the weak derivative is written .
[F1] is Banach under Countable Choice by Riesz-Fischer completeness of for ; for complex classes use Complex Lp completeness and almost-everywhere subsequences. in the translation convention of Translation of a function on ; each is linear, and the family is a strongly continuous semigroup of isometries: the functional equation is immediate and strong continuity at is the published translation-continuity theorem for , which assumes Countable Choice ( in as , for , The space as the quotient by null functions, The Axiom of Countable Choice ()).
[F2] Weak derivative: represents exactly when for every , and consists of the classes with (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).
[F3] Test functions lie in for the Hölder conjugate exponent , and (Conjugate exponents, including the endpoint conventions, Holder's inequality for integrals, including the endpoint cases).
[F4] Dominated convergence: pointwise convergence plus domination by one integrable function gives convergence of the integrals (Dominated convergence); Lebesgue measure and measurability are translation invariant, so for integrable (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).
[F5] The Bochner integral of a continuous -valued curve is defined, the norm inequality bounds it, is bounded linear on and therefore commutes with Bochner integrals, and averages of continuous curves converge to their endpoint values (Average convergence for a continuous Banach-valued function, Bounded linear maps commute with Bochner integration); Fubini applies to the absolutely integrable products below (Fubini's theorem for L^1 functions on a sigma-finite product).
[F6] The embedding of into distributions is injective on almost-everywhere classes: a locally integrable function pairing to zero against every test function vanishes almost everywhere (Locally integrable functions embed in distributions, which assumes Countable Choice).
[F7] The generator is defined by right difference quotients (Infinitesimal generator of a C0-semigroup, Strongly continuous semigroup).
Proof technique: direct: identify the difference quotients with averages of translates of the weak derivative, then identify the generator in both directions by test-function pairings.
is a strongly continuous semigroup of isometries: is linear, and hold pointwise, because translation preserves the integral of [F4], and in as by [F1].
Let and . The curve is continuous from to by [F1], so is defined by [F5], and as .
For and the difference quotient equals almost everywhere. Indeed, for every , translation invariance [F4] gives ; writing and applying Fubini [F5] and the weak-derivative identity of [F2] with the test function , ; by [F5] this equals . Two functions with the same pairing with every test function coincide almost everywhere by [F6].
Therefore as for every ; by the definition of the generator [F7], and for .
Conversely, suppose , so that in for some . For every , by [F3], so . On the other hand the identity of [step 1.3] (which used only ) gives , and for the integrand is supported in a fixed compact interval and bounded there by , whose integral over is finite because ; since pointwise, dominated convergence [F4] gives for every test function . By the definition of the weak derivative [F2], is the weak derivative of , so and almost everywhere.
Combining [step 2.1] and [step 2.2], the generator of the right-translation semigroup is with , and the difference quotients converge to in for every ; the semigroup is strongly continuous by [step 1.1]. The verification assumes Countable Choice, inherited from the translation-continuity and distribution-embedding inputs.
Depends on
- Complex Lp completeness and almost-everywhere subsequences
- Riesz-Fischer completeness of $L^p$ for $1 \le p \le \infty$
- Strongly continuous semigroup
- Infinitesimal generator of a C0-semigroup
- $\|\tau_h f - f\|_p \to 0$ in $L^p(\mathbb{R}^n)$ as $h \to 0$, for $1 \le p < \infty$
- The space $L^p(\mu)$ as the quotient by null functions
- Weak derivative of a locally integrable function
- Integer-order Sobolev spaces and their norms
- Meyers–Serrin density on an arbitrary open set
- Dominated convergence
- Translation of a function on $\mathbb{R}^n$
- Classical derivatives agree with weak derivatives
- Holder's inequality for integrals, including the endpoint cases
- Locally integrable functions embed in distributions
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Average convergence for a continuous Banach-valued function
- Bounded linear maps commute with Bochner integration
- Fubini's theorem for L^1 functions on a sigma-finite product
- Conjugate exponents, including the endpoint conventions
- Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
Used by
- A mild solution need not be classical Counterexample
- Strong continuity does not imply operator-norm continuity Counterexample
Dependency tree · two levels
99 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)
- 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)