2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
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-30 hoelzl 2014-05-30 generalizd measurability on restricted space; rule for integrability on compact sets
2014-05-30 hoelzl 2014-05-30 better support for restrict_space
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
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-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
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;
2013-03-22 hoelzl 2013-03-22 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)
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-07 hoelzl 2012-12-07 fundamental theorem of calculus for the Lebesgue integral
2012-12-05 hoelzl 2012-12-05 Remove looping rule from measurability prover
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 moved (b)choice_iff(') to Hilbert_Choice
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-10-10 hoelzl 2012-10-10 add induction for real Borel measurable functions
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from measure_eqI_generator_eq
2012-10-10 hoelzl 2012-10-10 remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10 hoelzl 2012-10-10 tuned Lebesgue measure proofs
2012-04-25 hoelzl 2012-04-25 equate positive Lebesgue integral and MV-Analysis' Gauge integral
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-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-03-30 hoelzl 2011-03-30 add lebesgue_real_affine
2011-03-29 hoelzl 2011-03-29 split Product_Measure into Binary_Product_Measure and Finite_Product_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 use measure_preserving in ..._vimage lemmas
2011-02-04 hoelzl 2011-02-04 prefer p2e before e2p; use measure_unique_Int_stable_vimage;
2011-02-04 hoelzl 2011-02-04 add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
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
2011-01-18 hoelzl 2011-01-18 Gauge measure removed
2011-01-14 hoelzl 2011-01-14 integral on lebesgue measure is extension of integral on borel measure
2010-12-08 hoelzl 2010-12-08 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
2010-12-08 hoelzl 2010-12-08 cleanup bijectivity btw. product spaces and pairs
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-02 hoelzl 2010-12-02 Moved theorems to appropriate place.
2010-12-01 hoelzl 2010-12-01 Generalized simple_functionD and less_SUP_iff. Moved theorems to appropriate places.
2010-12-01 hoelzl 2010-12-01 Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.