summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.

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.