Wed, 10 Oct 2012 12:12:23 +0200 | hoelzl | generalize from prob_space to finite_measure | changeset | files |
Wed, 10 Oct 2012 12:12:22 +0200 | hoelzl | add measurable_compose | changeset | files |
Wed, 10 Oct 2012 12:12:21 +0200 | hoelzl | simplified assumptions for kolmogorov_0_1_law | changeset | files |
Wed, 10 Oct 2012 12:12:21 +0200 | hoelzl | merge should operate on pairs | changeset | files |
Wed, 10 Oct 2012 12:12:20 +0200 | hoelzl | remove incseq assumption from sigma_prod_algebra_sigma_eq | changeset | files |
Wed, 10 Oct 2012 12:12:19 +0200 | hoelzl | sigma_finite_iff_density_finite does not require a positive density function | changeset | files |
Wed, 10 Oct 2012 12:12:18 +0200 | hoelzl | tuned Lebesgue measure proofs | changeset | files |
Wed, 10 Oct 2012 12:12:18 +0200 | hoelzl | tuned product measurability | changeset | files |