src/HOL/Probability/Probability_Measure.thy
Wed, 14 Jan 2015 09:59:12 +0100 Andreas Lochbihler allow line breaks in probability syntax
Tue, 13 Jan 2015 19:10:36 +0100 hoelzl measurability prover: removed app splitting, replaced by more powerful destruction rules
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;
Wed, 22 Oct 2014 13:58:30 +0200 Andreas Lochbihler add print translation for probability notation \<P>
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
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
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)
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Mon, 19 May 2014 14:26:58 +0200 hoelzl renamed positive_integral to nn_integral
Mon, 19 May 2014 13:44:13 +0200 hoelzl fixed document generation for HOL-Probability
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
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Tue, 12 Nov 2013 19:28:56 +0100 hoelzl measure of a countable union
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 07 Dec 2012 14:29:09 +0100 hoelzl add exponential and uniform distributions
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
Fri, 16 Nov 2012 14:46:23 +0100 hoelzl rules for AE and prob
Fri, 02 Nov 2012 14:23:54 +0100 hoelzl use measurability prover
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:31 +0200 hoelzl joint distribution of independent variables
Wed, 10 Oct 2012 12:12:26 +0200 hoelzl show and use distributed_swap and distributed_jointI
Wed, 10 Oct 2012 12:12:25 +0200 hoelzl continuous version of entropy_le
Wed, 10 Oct 2012 12:12:23 +0200 hoelzl generalize from prob_space to finite_measure
Wed, 10 Oct 2012 12:12:18 +0200 hoelzl tuned product measurability
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
Tue, 13 Mar 2012 16:56:56 +0100 wenzelm prefer abs_def over def_raw;
Tue, 13 Mar 2012 13:31:26 +0100 wenzelm tuned proofs -- eliminated pointless chaining of facts after 'interpret';
Tue, 28 Feb 2012 21:53:36 +0100 wenzelm avoid undeclared variables in let bindings;
Tue, 20 Dec 2011 11:40:56 +0100 noschinl add simp rules for enat and ereal
Wed, 07 Dec 2011 15:10:29 +0100 hoelzl remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
Thu, 01 Dec 2011 14:03:57 +0100 hoelzl moved theorems about distribution to the definition; removed oopsed-lemma
Thu, 01 Dec 2011 14:03:57 +0100 hoelzl rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Mon, 04 Jul 2011 10:23:46 +0200 hoelzl the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
Mon, 27 Jun 2011 09:42:46 +0200 hoelzl move conditional expectation to its own theory file
Thu, 09 Jun 2011 14:04:34 +0200 hoelzl lemma: independence is equal to mutual information = 0
Thu, 09 Jun 2011 13:55:11 +0200 hoelzl jensens inequality
Thu, 26 May 2011 20:51:03 +0200 hoelzl integral strong monotone; finite subadditivity for measure
Thu, 26 May 2011 17:40:01 +0200 hoelzl add lemma indep_distribution_eq_measure
Thu, 26 May 2011 14:11:57 +0200 hoelzl add lemma indep_sets_collect_sigma
Mon, 23 May 2011 19:21:05 +0200 hoelzl move lemmas to Extended_Reals and Extended_Real_Limits
Fri, 20 May 2011 21:38:32 +0200 hoelzl Add restricted borel measure to {0 .. 1}
Fri, 20 May 2011 16:23:03 +0200 hoelzl add lemma prob_finite_product
Thu, 19 May 2011 19:58:07 +0200 hoelzl add Bernoulli space
Thu, 19 May 2011 19:57:59 +0200 hoelzl add product of probability spaces with finite cardinality
Thu, 19 May 2011 18:11:15 +0200 hoelzl remove double sum_over_space_real_distribution
Fri, 01 Apr 2011 17:20:56 +0200 hoelzl remove unnecessary prob_preserving
Fri, 01 Apr 2011 17:20:33 +0200 hoelzl add prob_space_vimage
Tue, 29 Mar 2011 14:27:42 +0200 hoelzl rename Probability_Space to Probability_Measure
less more (0) tip