| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 11:29:47 +0100 |
immler |
qualified interpretation of sigma_algebra, to avoid name clashes
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 12:29:02 +0100 |
hoelzl |
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Thu, 15 Nov 2012 10:49:58 +0100 |
immler |
regularity of measures, therefore:
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 19:18:35 +0100 |
hoelzl |
add support for function application to measurability prover
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:23:54 +0100 |
hoelzl |
use measurability prover
|
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:30 +0200 |
hoelzl |
indep_vars does not need sigma-sets
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:23 +0200 |
hoelzl |
remove incseq assumption from measure_eqI_generator_eq
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:21 +0200 |
hoelzl |
simplified assumptions for kolmogorov_0_1_law
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:18 +0200 |
hoelzl |
tuned product measurability
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:14 +0200 |
hoelzl |
rename terminal_events to tail_event
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 21:53:36 +0100 |
wenzelm |
avoid undeclared variables in let bindings;
|
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, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 14:04:34 +0200 |
hoelzl |
lemma: independence is equal to mutual information = 0
|
file |
diff |
annotate
|
| Thu, 26 May 2011 17:59:39 +0200 |
hoelzl |
introduce independence of two random variables
|
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:12:06 +0200 |
hoelzl |
add lemma indep_rv_finite
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:12:02 +0200 |
hoelzl |
add lemma borel_0_1_law
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:12:00 +0200 |
hoelzl |
use abbrevitation events == sets M
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:11:58 +0200 |
hoelzl |
add lemma kolmogorov_0_1_law
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:11:57 +0200 |
hoelzl |
add lemma indep_sets_collect_sigma
|
file |
diff |
annotate
|
| Tue, 17 May 2011 11:47:36 +0200 |
hoelzl |
Add formalization of probabilistic independence for families of sets
|
file |
diff |
annotate
|