| #
bb368494 |
|
15-Aug-2019 |
paulson <lp15@cam.ac.uk> |
new material; rotated premises of Lim_transform_eventually
|
| #
e6ca3b44 |
|
17-Jul-2019 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and a bit of tidying
|
| #
5bbcd2e4 |
|
11-Jul-2018 |
paulson <lp15@cam.ac.uk> |
patched a continuity proof
|
| #
b15d33eb |
|
13-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Probability builds with new definitions
|
| #
d244f158 |
|
25-Apr-2017 |
paulson <lp15@cam.ac.uk> |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
| #
78a9e4a8 |
|
16-Sep-2016 |
hoelzl <none@none> |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
--HG--
extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222
|
| #
7baf2986 |
|
13-Jun-2016 |
hoelzl <none@none> |
Probability: tuned headers; cleanup Radon_Nikodym
--HG--
extra : rebase_source : b1923775a469aec44566a1d1da6c9d6e69cb0de4
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
79d3be54 |
|
14-Apr-2016 |
hoelzl <none@none> |
Probability: move emeasure and nn_integral from ereal to ennreal
--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|