| Mon, 27 Jun 2011 09:42:46 +0200 |
hoelzl |
move conditional expectation to its own theory file
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 14:04:34 +0200 |
hoelzl |
lemma: independence is equal to mutual information = 0
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 13:55:11 +0200 |
hoelzl |
jensens inequality
|
file |
diff |
annotate
|
| Thu, 26 May 2011 20:51:03 +0200 |
hoelzl |
integral strong monotone; finite subadditivity for measure
|
file |
diff |
annotate
|
| Thu, 26 May 2011 17:40:01 +0200 |
hoelzl |
add lemma indep_distribution_eq_measure
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:11:57 +0200 |
hoelzl |
add lemma indep_sets_collect_sigma
|
file |
diff |
annotate
|
| Mon, 23 May 2011 19:21:05 +0200 |
hoelzl |
move lemmas to Extended_Reals and Extended_Real_Limits
|
file |
diff |
annotate
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
Add restricted borel measure to {0 .. 1}
|
file |
diff |
annotate
|
| Fri, 20 May 2011 16:23:03 +0200 |
hoelzl |
add lemma prob_finite_product
|
file |
diff |
annotate
|
| Thu, 19 May 2011 19:58:07 +0200 |
hoelzl |
add Bernoulli space
|
file |
diff |
annotate
|
| Thu, 19 May 2011 19:57:59 +0200 |
hoelzl |
add product of probability spaces with finite cardinality
|
file |
diff |
annotate
|
| Thu, 19 May 2011 18:11:15 +0200 |
hoelzl |
remove double sum_over_space_real_distribution
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 17:20:56 +0200 |
hoelzl |
remove unnecessary prob_preserving
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 17:20:33 +0200 |
hoelzl |
add prob_space_vimage
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:42 +0200 |
hoelzl |
rename Probability_Space to Probability_Measure
|
file |
diff |
annotate
| base
|