Mercurial
isabelle
/ file revisions
summary

shortlog

changelog

graph

tags

branches

file
 revisions 
annotate

diff

rss
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
20101229
wenzelm
20101229
explicit file specifications  avoid secondary load path;
file

diff

annotate
20101203
hoelzl
20101203
it is known as the extended reals, not the infinite reals
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