| Sat, 10 Oct 2015 19:22:05 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 16:40:47 +0200 |
hoelzl |
Measures form a CCPO
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 10:48:20 +0200 |
hoelzl |
move disjoint sets to their own theory
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 14:11:01 +0200 |
Andreas Lochbihler |
add lemmas about restrict_space
|
file |
diff |
annotate
|
| Fri, 16 Jan 2015 10:59:15 +0100 |
hoelzl |
tuned measurability proofs
|
file |
diff |
annotate
|
| Thu, 15 Jan 2015 15:04:51 +0100 |
hoelzl |
piecewise measurability using restrict_space; cleanup Borel_Space
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 12:06:18 +0100 |
hoelzl |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 17:05:58 +0100 |
hoelzl |
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 14:02:24 +0200 |
hoelzl |
fix document generation for HOL-Probability
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 16:27:31 +0200 |
hoelzl |
add measure space for (coinductive) streams
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Fri, 30 May 2014 18:48:05 +0200 |
hoelzl |
generalizd measurability on restricted space; rule for integrability on compact sets
|
file |
diff |
annotate
|
| Fri, 30 May 2014 15:56:30 +0200 |
hoelzl |
better support for restrict_space
|
file |
diff |
annotate
|
| Tue, 20 May 2014 19:24:39 +0200 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
| Mon, 19 May 2014 13:44:13 +0200 |
hoelzl |
fixed document generation for HOL-Probability
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|
| Tue, 13 May 2014 11:35:47 +0200 |
hoelzl |
clean up Lebesgue integration
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Wed, 13 Nov 2013 09:37:00 +0100 |
hoelzl |
fix document generation for HOL-Probability
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:56 +0100 |
hoelzl |
measure of a countable union
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:56 +0100 |
hoelzl |
add restrict_space measure
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 10:35:37 +0200 |
Andreas Lochbihler |
make measure_of total
|
file |
diff |
annotate
|