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).
License:	BSD License

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2011: afp-Integration-2011-02-11.tar.gz Isabelle 2009-2: afp-Integration-2010-07-01.tar.gz Isabelle 2009-1: afp-Integration-2009-12-12.tar.gz Isabelle 2009: afp-Integration-2009-04-29.tar.gz Isabelle 2008: afp-Integration-2008-06-10.tar.gz Isabelle 2007: afp-Integration-2007-11-27.tar.gz Isabelle 2005: afp-Integration-2005-10-14.tar.gz Isabelle 2004: afp-Integration-2004-11-23.tar.gz Isabelle 2004: afp-Integration-2004-11-22.tar.gz