| Thu, 18 Aug 2011 13:36:58 -0700 |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file | diff | annotate |
| Tue, 19 Jul 2011 14:36:12 +0200 |
Rename extreal => ereal
|
file | diff | annotate |
| Thu, 09 Jun 2011 14:04:34 +0200 |
lemma: independence is equal to mutual information = 0
|
file | diff | annotate |
| Thu, 26 May 2011 17:59:39 +0200 |
introduce independence of two random variables
|
file | diff | annotate |
| Thu, 26 May 2011 17:40:01 +0200 |
add lemma indep_distribution_eq_measure
|
file | diff | annotate |
| Thu, 26 May 2011 14:12:06 +0200 |
add lemma indep_rv_finite
|
file | diff | annotate |
| Thu, 26 May 2011 14:12:02 +0200 |
add lemma borel_0_1_law
|
file | diff | annotate |
| Thu, 26 May 2011 14:12:00 +0200 |
use abbrevitation events == sets M
|
file | diff | annotate |
| Thu, 26 May 2011 14:11:58 +0200 |
add lemma kolmogorov_0_1_law
|
file | diff | annotate |
| Thu, 26 May 2011 14:11:57 +0200 |
add lemma indep_sets_collect_sigma
|
file | diff | annotate |
| Tue, 17 May 2011 11:47:36 +0200 |
Add formalization of probabilistic independence for families of sets
|
file | diff | annotate |