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