| Tue, 27 Aug 2013 16:06:27 +0200 |
hoelzl |
renamed inner_dense_linorder to dense_linorder
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 18:51:21 +0200 |
hoelzl |
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 15:43:22 +0100 |
hoelzl |
generalized lemmas in Extended_Real_Limits
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 16:35:07 +0100 |
immler |
eliminated union_closed_basis; cleanup Fin_Map
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 17:30:36 +0100 |
hoelzl |
move prod instantiation of second_countable_topology to its definition
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 17:29:04 +0100 |
hoelzl |
renamed countable_basis_space to second_countable_topology
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
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 13:48:40 +0100 |
immler |
based countable topological basis on Countable_Set
|
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
|
| Fri, 16 Nov 2012 12:10:02 +0100 |
hoelzl |
more measurability rules
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 11:22:22 +0100 |
immler |
allow arbitrary enumerations of basis in locale for generation of borel sets
|
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
|
| 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:16 +0200 |
hoelzl |
use continuity to show Borel-measurability
|
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
|
| Tue, 13 Mar 2012 16:56:56 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 21:53:36 +0100 |
wenzelm |
avoid undeclared variables in let bindings;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 14:10:19 +0200 |
hoelzl |
correct import path
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 14:06:06 +0200 |
hoelzl |
allow to build Probability and MV-Analysis with one ROOT.ML
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:00:00 -0700 |
huffman |
make HOL-Probability respect set/pred distinction
|
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:38:29 +0200 |
hoelzl |
add ereal to typeclass infinity
|
file |
diff |
annotate
|
| 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
|