20110314 
hoelzl 
20110314 
reworked Probability theory: measures are not type restricted to positive extended reals

file  diff  annotate 
20110314 
hoelzl 
20110314 
moved t2_spaces to HOL image

file  diff  annotate 
20110223 
hoelzl 
20110223 
log is borel measurable

file  diff  annotate 
20110114 
hoelzl 
20110114 
tuned formalization of subalgebra

file  diff  annotate 
20101208 
hoelzl 
20101208 
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand

file  diff  annotate 
20101208 
hoelzl 
20101208 
integral over setprod

file  diff  annotate 
20101208 
haftmann 
20101208 
work around problems with etaexpansion of equations

file  diff  annotate 
20101208 
haftmann 
20101208 
nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules

file  diff  annotate 
20101206 
hoelzl 
20101206 
folding on arbitrary Lebesgue integrable functions

file  diff  annotate 
20101206 
hoelzl 
20101206 
fixed spelling errors

file  diff  annotate 
20101203 
hoelzl 
20101203 
it is known as the extended reals, not the infinite reals

file  diff  annotate 
20101201 
hoelzl 
20101201 
Tuned setup for borel_measurable with min, max and psuminf.

file  diff  annotate 
20101201 
hoelzl 
20101201 
Replace algebra_eqI by algebra.equality;
Move sets_sigma_subset to Sigma_Algebra;

file  diff  annotate 
20101201 
hoelzl 
20101201 
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the RadonNikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.

file  diff  annotate  base 