src/HOL/Probability/Information.thy
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-08-05 hoelzl 2016-08-05 move measure theory from HOL-Probability to HOL-Multivariate_Analysis
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-14 hoelzl 2016-04-14 Probability: move emeasure and nn_integral from ereal to ennreal
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-13 hoelzl 2014-06-13 properties of normal distributed random variables (by Sudeep Kanav)
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-06-03 hoelzl 2014-06-03 use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 for the product measure it is enough if only one measure is sigma-finite
2012-10-11 hoelzl 2012-10-11 cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-10 hoelzl 2012-10-10 add finite entropy
2012-10-10 hoelzl 2012-10-10 continuous version of mutual_information_eq_entropy_conditional_entropy
2012-10-10 hoelzl 2012-10-10 remove unnecessary assumption from conditional_entropy_eq
2012-10-10 hoelzl 2012-10-10 alternative definition of conditional entropy
2012-10-10 hoelzl 2012-10-10 remove unneeded assumption from conditional_entropy_generic_eq
2012-10-10 hoelzl 2012-10-10 show and use distributed_swap and distributed_jointI
2012-10-10 hoelzl 2012-10-10 rule to show that conditional mutual information is non-negative in the continuous case
2012-10-10 hoelzl 2012-10-10 continuous version of entropy_le
2012-10-10 hoelzl 2012-10-10 simplified entropy_uniform
2012-10-10 hoelzl 2012-10-10 tuned product measurability
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-12-07 hoelzl 2011-12-07 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
2011-12-01 hoelzl 2011-12-01 moved theorems about distribution to the definition; removed oopsed-lemma
2011-12-01 hoelzl 2011-12-01 remove duplicate theorem setsum_real_distribution
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-06-27 hoelzl 2011-06-27 move conditional expectation to its own theory file
2011-06-09 hoelzl 2011-06-09 lemma: independence is equal to mutual information = 0
2011-03-29 hoelzl 2011-03-29 rename Probability_Space to Probability_Measure
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-02-23 hoelzl 2011-02-23 add lemma KL_divergence_vimage, mutual_information_generic
2011-02-02 hoelzl 2011-02-02 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.
2011-01-24 hoelzl 2011-01-24 use pre-image measure, instead of image