| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Thu, 26 May 2011 20:49:56 +0200 |
hoelzl |
composition of convex and measurable function is measurable
|
file |
diff |
annotate
|
| Mon, 23 May 2011 19:21:05 +0200 |
hoelzl |
move lemmas to Extended_Reals and Extended_Real_Limits
|
file |
diff |
annotate
|
| Tue, 17 May 2011 12:21:58 +0200 |
hoelzl |
add borel_eq_atLeastLessThan
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 17:30:26 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:06:10 +0100 |
hoelzl |
standardized headers
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:49 +0100 |
hoelzl |
reworked Probability theory: measures are not type restricted to positive extended reals
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:33 +0100 |
hoelzl |
moved t2_spaces to HOL image
|
file |
diff |
annotate
|
| Wed, 23 Feb 2011 11:33:45 +0100 |
hoelzl |
log is borel measurable
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:56:42 +0100 |
hoelzl |
tuned formalization of subalgebra
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 19:32:11 +0100 |
hoelzl |
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 16:15:14 +0100 |
hoelzl |
integral over setprod
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 16:47:45 +0100 |
haftmann |
work around problems with eta-expansion of equations
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 14:52:23 +0100 |
haftmann |
nice syntax for lattice INFI, SUPR;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 19:54:56 +0100 |
hoelzl |
folding on arbitrary Lebesgue integrable functions
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 19:54:53 +0100 |
hoelzl |
fixed spelling errors
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 15:25:14 +0100 |
hoelzl |
it is known as the extended reals, not the infinite reals
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:12:53 +0100 |
hoelzl |
Tuned setup for borel_measurable with min, max and psuminf.
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:09:41 +0100 |
hoelzl |
Replace algebra_eqI by algebra.equality;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 19:20:30 +0100 |
hoelzl |
Support product spaces on sigma finite measures.
|
file |
diff |
annotate
| base
|