| Thu, 26 May 2011 22:02:40 +0200 | boehmes | iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette) | changeset | files |
| Thu, 26 May 2011 20:51:03 +0200 | hoelzl | integral strong monotone; finite subadditivity for measure | changeset | files |
| Thu, 26 May 2011 20:49:56 +0200 | hoelzl | composition of convex and measurable function is measurable | changeset | files |
| Thu, 26 May 2011 17:59:39 +0200 | hoelzl | introduce independence of two random variables | changeset | files |
| Thu, 26 May 2011 17:40:01 +0200 | hoelzl | add lemma indep_distribution_eq_measure | changeset | files |
| Thu, 26 May 2011 14:12:06 +0200 | hoelzl | add lemma indep_rv_finite | changeset | files |