Integration theory and random variables


Title: Integration theory and random variables
Author: Stefan Richter
Submission date: 2004-11-19
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.
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).
  author  = {Stefan Richter},
  title   = {Integration theory and random variables},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2004,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License