Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

A multiplication semigroup with an unbounded generator

Example

Assume Countable Choice. Let 1≤p<∞, X=Lp(0,∞) and q(s):=−s. For t≥0 define (T(t)f)(s):=etq(s)f(s)=e−tsf(s) (The space Lp(μ) as the quotient by null functions). Then (T(t))t≥0 is a strongly continuous semigroup of contractions on X, and its generator is the multiplication operator Af=qf,D(A)={f∈Lp(0,∞): qf∈Lp(0,∞)}={f: sf∈Lp(0,∞)}, which is unbounded: D(A)≠X.

Verification

Given: Countable Choice; 1≤p<∞; X=Lp(0,∞); q(s)=−s; (T(t)f)(s)=e−tsf(s) for t≥0.

[F1] X=Lp(0,∞) is Banach under Countable Choice by Riesz-Fischer completeness of Lp for 1≤p≤∞ for real classes and Complex Lp completeness and almost-everywhere subsequences for complex classes; the classes are those of The space Lp(μ) as the quotient by null functions; the Bochner/absolute-continuity framework used below is set up under Countable Choice (The Axiom of Countable Choice (ACω)).

[F2] Dominated convergence for the Lebesgue integral, including its use to compute Lp limits of scalar functions from pointwise convergence and a dominating Lp function (Dominated convergence).

[F3] The embedding of Lloc1(0,∞) into distributions is injective on almost-everywhere classes: a locally integrable function pairing to zero against every test function in Cc∞(0,∞) vanishes almost everywhere (Locally integrable functions embed in distributions).

[F4] The generator is defined by one-sided difference quotients, and unboundedness means that no finite constant bounds ∥Af∥ by ∥f∥ on D(A) (Infinitesimal generator of a C0-semigroup, Strongly continuous semigroup).

Proof technique: direct: pointwise computation for the semigroup and its difference quotients, dominated convergence for both inclusions of the generator domain, and a bump-function family for unboundedness.

1.1F1algebra

For every t≥0 the map T(t) is linear and ∥T(t)f∥pp=∫0∞e−tps∣f(s)∣p ds≤∥f∥pp, so T(t) is a contraction; the pointwise identities e−(t+r)s=e−tse−rs and e0=1 give T(t+r)=T(t)T(r) and T(0)=I.

2.1F2step 1.1

Strong continuity: for fixed f∈X, ∥T(t)f−f∥pp=∫0∞∣e−ts−1∣p∣f(s)∣p ds→0 as t↓0 by [F2], since e−ts→1 pointwise and ∣e−ts−1∣p≤2p for t≥0, so the integrand is dominated by the L1 function 2p∣f∣p.

3.1F2F4step 2.1

Inclusion {qf∈X}⊆D(A): if qf∈X, then ∥T(h)f−fh−qf∥pp=∫0∞∣e−hs−1h+s∣p∣f(s)∣p ds→0 by [F2], because e−hs−1h→−s pointwise and, by the inequality 1−e−x≤x for x≥0, the bracket is at most 2s, so the integrand is dominated by (2s∣f∣)p∈L1.

4.1F2F3step 3.1

Converse: suppose the difference quotients converge in X to some g, and let φ∈Cc∞(0,∞). By [F2] and the boundedness of s on supp⁡φ, ∫0∞e−hs−1hfφ ds→−∫0∞sfφ ds, while ∫0∞T(h)f−fhφ ds→∫0∞gφ ds because ∥T(h)f−fh−g∥p→0 and φ∈Lp′; hence ∫0∞(g−qf)φ ds=0 for every test function. The locally integrable function g−qf has sf∈Lloc1(0,∞), so [F3] gives g=qf almost everywhere; in particular qf=g∈X and f∈D(A) with Af=qf.

5.1F4step 4.1

Unboundedness and proper domain: for n≥1 let fn be the normalised nonnegative bump supported in [n,n+1] with ∥fn∥p=1. Then ∥Afn∥pp=∫nn+1sp∣fn(s)∣p ds≥np, so ∥Afn∥p≥n→∞ while ∥fn∥p=1, and no constant bounds A on its domain. Moreover D(A)≠X: the function f(s):=s−1−1/p1(1,∞) lies in Lp(0,∞) because ∫1∞s−p−1ds=1/p, while sf(s)=s−1/p is not in Lp because ∫1∞s−1ds=∞, so f∈X∖D(A).

6.1step 1.1step 2.1step 4.1step 5.1∎

Together with [step 1.1] and [step 2.1], the displayed claims follow: T is a strongly continuous contraction semigroup on Lp(0,∞) whose generator has domain {f:qf∈X}={f:sf∈Lp} and acts by Af=qf=−sf, and this operator is unbounded.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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