[Intention]: OneParameterSemigroups — representation theorems (Bernstein / Bochner / BCR)

[kim-em]

Roadmap area

OneParameterSemigroups

Items in scope

The representation theorems built on top of the object API:

• Bernstein: completely monotone on [0,∞) iff the Laplace transform of a unique finite measure
• Bochner on a finite-dimensional inner-product space: continuous positive-definite iff the Fourier transform of a finite measure
• BCR semigroup–Bochner (Berg–Christensen–Ressel 4.1.13): existence + uniqueness over ℝ≥0 × V

Notes

Proposed for Michael R Douglas's group (mrdouglasny/hille-yosida). See #16.

[mrdouglasny]

claim 3w
Representation theorems (Bernstein / Bochner / BCR) on top of the Parts B/C object API, ported from the sorry-free, axiom-free mrdouglasny/hille-yosida + a Bochner–Minlos development (per the division of labour in #16). Starting with Bernstein.

[github-actions]

@mrdouglasny you've claimed this task — it expires 2026-07-14 13:36 UTC.

[github-actions]

⌛ This claim expired (was due 2026-07-14 13:36 UTC) and has been released back to Unclaimed. Comment claim to pick it up again.