# 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). BibTeX: @article{Integration-AFP, author = {Stefan Richter}, title = {Integration theory and random variables}, journal = {Archive of Formal Proofs}, month = nov, year = 2004, note = {\url{https://isa-afp.org/entries/Integration.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License