| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 15:43:22 +0100 |
hoelzl |
generalized lemmas in Extended_Real_Limits
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:30 +0100 |
hoelzl |
use order topology for extended reals
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 14:29:09 +0100 |
hoelzl |
add exponential and uniform distributions
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 15:59:08 +0100 |
hoelzl |
Move the measurability prover to its own file
|
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
|
| Thu, 15 Nov 2012 10:49:58 +0100 |
immler |
regularity of measures, therefore:
|
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:27 +0200 |
hoelzl |
add induction rule for intersection-stable 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:15 +0200 |
hoelzl |
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 19:26:27 +0200 |
hoelzl |
add Caratheodories theorem for semi-rings of sets
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 19:26:00 +0200 |
hoelzl |
moved lemmas to appropriate places
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|