SHSLib

A Lean 4 / Mathlib formalization of Stochastic Hybrid Systems (SHS) — discrete-mode, continuous-state processes that mix ordinary differential flow with random jumps (mode switches and state resets), as introduced by Hespanha (2005) and built on Davis's theory of Piecewise-Deterministic Markov Processes (PDMPs).

The extended generator

An SHS evolves in mode and continuous state , flowing according to between jumps, and jumping to mode / state with intensity , for .

For a test function , the extended generator is defined as

The first two terms capture drift along the deterministic flow; the sum captures the expected jump contribution across all transition types.

Differential form. Along a sample path of the SHS,

Integral form. Equivalently,

These identities (SHS.eq10_differential_generator_formula and SHS.theorem1_generator_formula in SHSLib/Core/Generator.lean) are the basis for deriving moment ODEs and the Fokker–Planck equation for the state density.

Structure

Module	Contents
`SHSLib.Core.Basic`	SHS structure, assumptions, flow
`SHSLib.Core.Generator`	Extended generator , moment evolution, Fokker–Planck equation
`SHSLib.Foundations.DavisCh1`	Measure theory, probability, and stochastic-process foundations
`SHSLib.Foundations.DavisCh2`	Piecewise-Deterministic Markov Process (PDMP) theory

Building

lake build

Requires Lean 4 and Mathlib (pinned via lakefile.toml).

Documentation

Per-module notes are in wiki/index.md — what each module proves, its key theorems and definitions, and remaining gaps.

References

M. H. A. Davis, Markov Models and Optimization, Chapman & Hall, 1993.
J. P. Hespanha, "A model for stochastic hybrid systems with application to communication networks," Nonlinear Analysis, 2005.

License

MIT — see LICENSE.