src/HOL/Probability/Measure_Space.thy
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Mon, 17 Nov 2014 18:19:06 +0100 hoelzl add reindex rules for distr and nn_integral on count_space
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Tue, 07 Oct 2014 10:34:24 +0200 hoelzl add Giry monad
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
Mon, 30 Jun 2014 15:45:03 +0200 hoelzl some lemmas about the indicator function; removed lemma sums_def2
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
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
Thu, 12 Jun 2014 15:47:36 +0200 hoelzl properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
Fri, 30 May 2014 15:56:30 +0200 hoelzl better support for restrict_space
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Mon, 19 May 2014 13:44:13 +0200 hoelzl fixed document generation for HOL-Probability
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Tue, 18 Mar 2014 15:53:48 +0100 hoelzl cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Tue, 12 Nov 2013 19:28:56 +0100 hoelzl add restrict_space measure
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 05 Mar 2013 15:43:22 +0100 hoelzl generalized lemmas in Extended_Real_Limits
Thu, 31 Jan 2013 11:31:30 +0100 hoelzl use order topology for extended reals
Fri, 07 Dec 2012 14:29:09 +0100 hoelzl add exponential and uniform distributions
Wed, 05 Dec 2012 15:59:08 +0100 hoelzl Move the measurability prover to its own file
Tue, 27 Nov 2012 11:29:47 +0100 immler qualified interpretation of sigma_algebra, to avoid name clashes
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Thu, 15 Nov 2012 10:49:58 +0100 immler regularity of measures, therefore:
Fri, 02 Nov 2012 14:23:40 +0100 hoelzl add measurability prover; add support for Borel sets
Fri, 02 Nov 2012 14:00:39 +0100 hoelzl add syntax and a.e.-rules for (conditional) probability on predicates
Wed, 10 Oct 2012 12:12:27 +0200 hoelzl add induction rule for intersection-stable sigma-sets
Wed, 10 Oct 2012 12:12:23 +0200 hoelzl remove incseq assumption from measure_eqI_generator_eq
Wed, 10 Oct 2012 12:12:15 +0200 hoelzl tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
Wed, 25 Apr 2012 19:26:27 +0200 hoelzl add Caratheodories theorem for semi-rings of sets
Wed, 25 Apr 2012 19:26:00 +0200 hoelzl moved lemmas to appropriate places
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
less more (0) tip