| Wed, 10 Apr 2013 18:51:21 +0200 |
hoelzl |
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 14:29:09 +0100 |
hoelzl |
add exponential and uniform distributions
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 11:29:47 +0100 |
immler |
qualified interpretation of sigma_algebra, to avoid name clashes
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
rules for AE and prob
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:23:54 +0100 |
hoelzl |
use measurability prover
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:23:40 +0100 |
hoelzl |
add measurability prover; add support for Borel sets
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:00:39 +0100 |
hoelzl |
add syntax and a.e.-rules for (conditional) probability on predicates
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:31 +0200 |
hoelzl |
joint distribution of independent variables
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:26 +0200 |
hoelzl |
show and use distributed_swap and distributed_jointI
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:25 +0200 |
hoelzl |
continuous version of entropy_le
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:23 +0200 |
hoelzl |
generalize from prob_space to finite_measure
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:18 +0200 |
hoelzl |
tuned product measurability
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:56:56 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 13:31:26 +0100 |
wenzelm |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 21:53:36 +0100 |
wenzelm |
avoid undeclared variables in let bindings;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 11:40:56 +0100 |
noschinl |
add simp rules for enat and ereal
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 15:10:29 +0100 |
hoelzl |
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:03:57 +0100 |
hoelzl |
moved theorems about distribution to the definition; removed oopsed-lemma
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:03:57 +0100 |
hoelzl |
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 10:23:46 +0200 |
hoelzl |
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
|
file |
diff |
annotate
|
| 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
|