Mercurial
isabelle
/ file revisions
summary

shortlog

changelog

graph

tags

branches

file
 revisions 
annotate

diff

rss
src/HOL/Probability/Complete_Measure.thy
20101208
hoelzl
20101208
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
file

diff

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

diff

annotate
20101201
hoelzl
20101201
Generalized simple_functionD and less_SUP_iff. Moved theorems to appropriate places.
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