Integration theory and random variables

Stefan Richter 🌐

November 19, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Lebesgue-style integration plays a major role in advanced probability. We formalize concepts of elementary measure theory, real-valued random variables as Borel-measurable functions, and a stepwise inductive definition of the integral itself. All proofs are carried out in human readable style using the Isar language.


BSD License

This article is of historical interest only. Lebesgue-style integration and probability theory are now available as part of the Isabelle/HOL distribution (directory Probability).


Session Integration