src/HOL/Probability/Borel_Space.thy
 2011-01-14 hoelzl 2011-01-14 tuned formalization of subalgebra file | diff | annotate 2010-12-08 hoelzl 2010-12-08 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand file | diff | annotate 2010-12-08 hoelzl 2010-12-08 integral over setprod file | diff | annotate 2010-12-08 haftmann 2010-12-08 work around problems with eta-expansion of equations file | diff | annotate 2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules file | diff | annotate 2010-12-06 hoelzl 2010-12-06 folding on arbitrary Lebesgue integrable functions file | diff | annotate 2010-12-06 hoelzl 2010-12-06 fixed spelling errors file | diff | annotate 2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals file | diff | annotate 2010-12-01 hoelzl 2010-12-01 Tuned setup for borel_measurable with min, max and psuminf. file | diff | annotate 2010-12-01 hoelzl 2010-12-01 Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra; file | diff | annotate 2010-12-01 hoelzl 2010-12-01 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 Radon-Nikodym 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