hoelzl [Wed, 10 Oct 2012 12:12:25 +0200] rev 49786
continuous version of entropy_le
hoelzl [Wed, 10 Oct 2012 12:12:24 +0200] rev 49785
simplified entropy_uniform
hoelzl [Wed, 10 Oct 2012 12:12:23 +0200] rev 49784
remove incseq assumption from measure_eqI_generator_eq
hoelzl [Wed, 10 Oct 2012 12:12:23 +0200] rev 49783
generalize from prob_space to finite_measure
hoelzl [Wed, 10 Oct 2012 12:12:22 +0200] rev 49782
add measurable_compose
hoelzl [Wed, 10 Oct 2012 12:12:21 +0200] rev 49781
simplified assumptions for kolmogorov_0_1_law
hoelzl [Wed, 10 Oct 2012 12:12:21 +0200] rev 49780
merge should operate on pairs
hoelzl [Wed, 10 Oct 2012 12:12:20 +0200] rev 49779
remove incseq assumption from sigma_prod_algebra_sigma_eq
hoelzl [Wed, 10 Oct 2012 12:12:19 +0200] rev 49778
sigma_finite_iff_density_finite does not require a positive density function
hoelzl [Wed, 10 Oct 2012 12:12:18 +0200] rev 49777
tuned Lebesgue measure proofs