| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
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:13:51 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:17:22 +0100 |
Andreas Lochbihler |
add another lemma to split nn_integral over product count_space
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:05:21 +0100 |
Andreas Lochbihler |
nn_integral can be split over arbitrary product count_spaces
|
file |
diff |
annotate
|
| Fri, 23 Jan 2015 12:04:27 +0100 |
hoelzl |
integral of the product of count spaces equals the integral of the count space of the product type
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 19:10:36 +0100 |
hoelzl |
measurability prover: removed app splitting, replaced by more powerful destruction rules
|
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 10:34:24 +0200 |
hoelzl |
add Giry monad
|
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
|
| Thu, 12 Jun 2014 15:47:36 +0200 |
hoelzl |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
| Tue, 20 May 2014 19:24:39 +0200 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
| Mon, 19 May 2014 14:26:58 +0200 |
hoelzl |
renamed positive_integral to nn_integral
|
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
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
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, 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 |
for the product measure it is enough if only one measure is sigma-finite
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 14:38:58 +0200 |
hoelzl |
cleanup borel_measurable_positive_integral_(fst|snd)
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:34 +0200 |
hoelzl |
induction prove for positive_integral_fst
|
file |
diff |
annotate
|