src/HOL/Probability/Lebesgue_Measure.thy
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2015-01-14 Andreas Lochbihler 2015-01-14 allow line breaks in integral notation
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
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