hoelzl [Wed, 10 Oct 2012 12:12:36 +0200] rev 49802
continuous version of mutual_information_eq_entropy_conditional_entropy
hoelzl [Wed, 10 Oct 2012 12:12:35 +0200] rev 49801
add induction for real Borel measurable functions
hoelzl [Wed, 10 Oct 2012 12:12:34 +0200] rev 49800
induction prove for positive_integral_fst
hoelzl [Wed, 10 Oct 2012 12:12:34 +0200] rev 49799
strong nonnegativ (instead of ae nn) for induction rule
hoelzl [Wed, 10 Oct 2012 12:12:33 +0200] rev 49798
induction prove for positive_integral_density
hoelzl [Wed, 10 Oct 2012 12:12:32 +0200] rev 49797
add induction rules for simple functions and for Borel measurable functions
hoelzl [Wed, 10 Oct 2012 12:12:32 +0200] rev 49796
introduce induction rules for simple functions and for Borel measurable functions
hoelzl [Wed, 10 Oct 2012 12:12:31 +0200] rev 49795
joint distribution of independent variables
hoelzl [Wed, 10 Oct 2012 12:12:30 +0200] rev 49794
indep_vars does not need sigma-sets
hoelzl [Wed, 10 Oct 2012 12:12:29 +0200] rev 49793
simplified definitions
hoelzl [Wed, 10 Oct 2012 12:12:29 +0200] rev 49792
remove unnecessary assumption from conditional_entropy_eq
hoelzl [Wed, 10 Oct 2012 12:12:28 +0200] rev 49791
alternative definition of conditional entropy
hoelzl [Wed, 10 Oct 2012 12:12:27 +0200] rev 49790
remove unneeded assumption from conditional_entropy_generic_eq
hoelzl [Wed, 10 Oct 2012 12:12:27 +0200] rev 49789
add induction rule for intersection-stable sigma-sets
hoelzl [Wed, 10 Oct 2012 12:12:26 +0200] rev 49788
show and use distributed_swap and distributed_jointI
hoelzl [Wed, 10 Oct 2012 12:12:25 +0200] rev 49787
rule to show that conditional mutual information is non-negative in the continuous case
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
hoelzl [Wed, 10 Oct 2012 12:12:18 +0200] rev 49776
tuned product measurability
hoelzl [Wed, 10 Oct 2012 12:12:17 +0200] rev 49775
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl [Wed, 10 Oct 2012 12:12:16 +0200] rev 49774
use continuity to show Borel-measurability
hoelzl [Wed, 10 Oct 2012 12:12:15 +0200] rev 49773
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs