| #
e6ca3b44 |
|
17-Jul-2019 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and a bit of tidying
|
| #
48a391b7 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
| #
b15d33eb |
|
13-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Probability builds with new definitions
|
| #
246d8de3 |
|
28-Feb-2017 |
paulson <lp15@cam.ac.uk> |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
a1e8064f |
|
13-Oct-2016 |
hoelzl <none@none> |
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
--HG--
extra : rebase_source : 55f4bbfc342a2532835d5bd35b92dd5cf39bc512
|
| #
05ddf657 |
|
02-Oct-2016 |
wenzelm <none@none> |
updated headers;
|
| #
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
|
| #
9e5f909f |
|
05-Aug-2016 |
hoelzl <none@none> |
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
--HG--
rename : src/HOL/Probability/Binary_Product_Measure.thy => src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy
rename : src/HOL/Probability/Bochner_Integration.thy => src/HOL/Multivariate_Analysis/Bochner_Integration.thy
rename : src/HOL/Probability/Borel_Space.thy => src/HOL/Multivariate_Analysis/Borel_Space.thy
rename : src/HOL/Probability/Caratheodory.thy => src/HOL/Multivariate_Analysis/Caratheodory.thy
rename : src/HOL/Probability/Complete_Measure.thy => src/HOL/Multivariate_Analysis/Complete_Measure.thy
rename : src/HOL/Probability/Embed_Measure.thy => src/HOL/Multivariate_Analysis/Embed_Measure.thy
rename : src/HOL/Probability/Finite_Product_Measure.thy => src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy
rename : src/HOL/Probability/Interval_Integral.thy => src/HOL/Multivariate_Analysis/Interval_Integral.thy
rename : src/HOL/Probability/Lebesgue_Integral_Substitution.thy => src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy
rename : src/HOL/Probability/Lebesgue_Measure.thy => src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy
rename : src/HOL/Probability/Measurable.thy => src/HOL/Multivariate_Analysis/Measurable.thy
rename : src/HOL/Probability/Measure_Space.thy => src/HOL/Multivariate_Analysis/Measure_Space.thy
rename : src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy => src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy
rename : src/HOL/Probability/Radon_Nikodym.thy => src/HOL/Multivariate_Analysis/Radon_Nikodym.thy
rename : src/HOL/Probability/Regularity.thy => src/HOL/Multivariate_Analysis/Regularity.thy
rename : src/HOL/Probability/Set_Integral.thy => src/HOL/Multivariate_Analysis/Set_Integral.thy
rename : src/HOL/Probability/Sigma_Algebra.thy => src/HOL/Multivariate_Analysis/Sigma_Algebra.thy
rename : src/HOL/Probability/measurable.ML => src/HOL/Multivariate_Analysis/measurable.ML
extra : rebase_source : 30ab39c42165c1c5622833cf256065cbfff030f9
|
| #
eb030641 |
|
02-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
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;
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|