Integration Theory and Random Variables

Stefan Richter

19 November 2004

Abstract

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

Note

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).

Topics

Theories

Cite

×
@article{Integration-AFP,
  author  = {Stefan Richter},
  title   = {Integration theory and random variables},
  journal = {Archive of Formal Proofs},
  month   = November,
  year    = 2004,
  note    = {\url{http://isa-afp.org/entries/Integration.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download