| #
3aaddd80 |
|
18-Aug-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Added integral_add_lemma' and thus finished the "correct" FUBINI!
|
| #
2df08d14 |
|
27-Jul-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Removed some duplicated theorems due to code merging issues ...
|
| #
53b53540 |
|
26-Jul-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Fubini's Theorem (martingaleTheory.FUBINI) + variants in some models of extreals
|
| #
b74542ef |
|
13-Jul-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Fixed tailing white-spaces and Unicode violations
|
| #
b76bf21d |
|
13-Jul-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Lemmas about r.v.'s having identical distribution
|
| #
c0ca1d19 |
|
28-May-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Product measure and Tonelli's theorem
|
| #
49d03295 |
|
09-Feb-2020 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Radon-Nikodym Theorem for [0,+Inf]-Measure Theory (HVG concordia)
|
| #
51d49003 |
|
20-Sep-2019 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Re-defined ext_suminf (extrealTheory), only specified for positive functions;
Stop generating HTML files for probability scripts.
|
| #
c4db120b |
|
19-Sep-2019 |
Chun Tian <binghe.lisp@gmail.com> |
The new HOL-Probability based on [0,+Inf]-measure theory (#735)
* The new HOL-Probability based on [0,+Inf]-measure theory
* Noted the new HOL-Probability in next-release notes;
Added a dedicated README.md in `src/probability`.
|