Open Research Index

MarkovProcess

Scott Armstrong

Palomar Registrypalomar/PALOMAR-2026-09-15-000007Sep 15, 2026math.PRscore 0

A Lean formalization of continuous-path Markov processes associated with conservative Feller transition semigroups on nonempty locally compact Polish spaces. A uniform Kolmogorov displacement-moment bound yields a unique measurable kernel from each starting point to continuous-path space, with the prescribed finite-dimensional distributions. The library also develops strong Markov properties, generators and resolvents, stopping and killing, and Brownian motion as an example. The existence and uniqueness theorem is independently checked using Audit/ContinuousMarkovProcess/comparator.json.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-15-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-15-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-15-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'