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.

The right-translation semigroup on Lp has the weak derivative as generator

Example

Assume Countable Choice (The Axiom of Countable Choice (ACω)). Let 1≤p<∞ and X=Lp(R) (The space Lp(μ) as the quotient by null functions). For t≥0 and f∈X define (T(t)f)(s):=f(s+t) (the right translation, represented on the a.e. class by Translation of a function on Rn). Then (T(t))t≥0 is a strongly continuous semigroup of isometries on X (each T(t) has norm 1), and its generator is Af=f′withD(A)=W1,p(R)={f∈Lp(R): f′∈Lp(R)}, the derivative being the weak derivative (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms). Moreover ∥T(h)f−fh−f′∥p→0 for every f∈W1,p(R).

Verification

Given: Countable Choice; 1≤p<∞; X=Lp(R); (T(t)f)(s)=f(s+t) for t≥0; f∈X; for f∈W1,p(R) the weak derivative is written f′.

[F1] Lp(R;R) is Banach under Countable Choice by Riesz-Fischer completeness of Lp for 1≤p≤∞; for complex classes use Complex Lp completeness and almost-everywhere subsequences. T(t)=τ−t in the translation convention of Translation of a function on Rn; each T(t) is linear, and the family is a strongly continuous semigroup of isometries: the functional equation is immediate and strong continuity at 0 is the published translation-continuity theorem for 1≤p<∞, which assumes Countable Choice (∥τhf−f∥p→0 in Lp(Rn) as h→0, for 1≤p<∞, The space Lp(μ) as the quotient by null functions, The Axiom of Countable Choice (ACω)).

[F2] Weak derivative: v represents D1f exactly when ∫Rfφ′=−∫Rvφ for every φ∈Cc∞(R), and W1,p(R) consists of the Lp classes with f′∈Lp (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).

[F3] Test functions lie in Lp′ for the Hölder conjugate exponent p′, and ∣∫hφ∣≤∥h∥p∥φ∥p′ (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 ∫h(s+t) ds=∫h(s) ds for integrable h (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[F5] The Bochner integral of a continuous Lp-valued curve is defined, the norm inequality bounds it, Λφ(h):=∫hφ is bounded linear on Lp 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 Lloc1(R) 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.

1.1F1F4

T is a strongly continuous semigroup of isometries: T(t) is linear, T(t+s)f=T(t)T(s)f and T(0)=I hold pointwise, ∥T(t)f∥p=∥f∥p because translation preserves the integral of ∣f∣p [F4], and T(t)f→f in Lp as t↓0 by [F1].

1.2F1F5

Let f∈W1,p(R) and h>0. The curve u↦τ−uf′ is continuous from [0,h] to Lp by [F1], so Mh:=1h∫0hτ−uf′ du∈Lp is defined by [F5], and ∥Mh−f′∥p≤sup⁡0≤u≤h∥τ−uf′−f′∥p→0 as h↓0.

1.3F2F4F5F6

For f∈W1,p and h>0 the difference quotient qh:=T(h)f−fh∈Lp equals Mh almost everywhere. Indeed, for every φ∈Cc∞(R), translation invariance [F4] gives ∫Rqhφ=1h(∫Rf(s)φ(s−h) ds−∫Rf(s)φ(s) ds)=1h∫Rf(s)(φ(s−h)−φ(s))ds; writing φ(s−h)−φ(s)=−∫0hφ′(s−u) du and applying Fubini [F5] and the weak-derivative identity of [F2] with the test function φ(⋅−u), ∫Rqhφ=−1h∫0h∫Rf(s)φ′(s−u) ds du=1h∫0h∫Rf′(s)φ(s−u) ds du=1h∫0hΛφ(τ−uf′) du; by [F5] this equals Λφ(Mh)=∫RMhφ. Two Lp functions with the same pairing with every test function coincide almost everywhere by [F6].

2.1F7step 1.2step 1.3

Therefore ∥T(h)f−fh−f′∥p=∥Mh−f′∥p→0 as h↓0 for every f∈W1,p(R); by the definition of the generator [F7], W1,p(R)⊆D(A) and Af=f′ for f∈W1,p(R).

2.2F2F3F4step 1.3

Conversely, suppose f∈D(A), so that qh→g in Lp for some g. For every φ∈Cc∞(R), ∣∫(qh−g)φ∣≤∥qh−g∥p∥φ∥p′→0 by [F3], so ∫gφ=lim⁡h∫qhφ. On the other hand the identity of [step 1.3] (which used only f∈Lp) gives ∫qhφ=1h∫f(s)(φ(s−h)−φ(s))ds, and for 0<h≤1 the integrand is supported in a fixed compact interval K and bounded there by ∣f∣sup⁡K∣φ′∣, whose integral over K is finite because f∈Lp(K)⊆L1(K); since φ(s−h)−φ(s)h→−φ′(s) pointwise, dominated convergence [F4] gives ∫gφ=−∫fφ′ for every test function φ. By the definition of the weak derivative [F2], g is the weak derivative of f, so f∈W1,p(R) and g=f′ almost everywhere.

3.1F1F6step 1.1step 2.1step 2.2∎

Combining [step 2.1] and [step 2.2], the generator of the right-translation semigroup is Af=f′ with D(A)=W1,p(R), and the difference quotients converge to f′ in Lp for every f∈W1,p(R); 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

Used by

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