src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 37489 44e42d392c6e
child 41654 32fe42892983
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
wenzelm@33267
     1
theory Multivariate_Analysis
hoelzl@38656
     2
imports Fashoda Gauge_Measure
himmelma@33175
     3
begin
himmelma@33175
     4
himmelma@33175
     5
end