Added extreal-based Borel measure space (ext_lborel)

Fubini's Theorem (martingaleTheory.FUBINI) + variants in some models of extreals

Adjusted expectation_distribution and prob_space_def

Lemmas about r.v.'s having identical distribution

Product measure and Tonelli's theorem

Updated HOL Description for mathematical theories (with other cumulative fixes)

Strong Law of Large Numbers for uncorrelated r.v.'s (SLLN_uncorrelated)

More ℝ-normalisation, removing inverted factors where possible

Previously, the code would collect up

...x... <= ... x...

for various possible exponents of x, but the normalisation would only
trigger if the x was present on both sides. Now, if the exponent is
negative, a lone x will shift to the other side of the relation
regardless.

This applies also to fractions, so that

x <= 3/4 * y

will turn into

4 * x <= 3 * y

Fixes in src/probability and more explicit regression tests.

Removed "Reverse" from hurdUtils, using "Tactical.reverse" instead

Fixed WLLN_uncorrelated_L2 due to real normalization after 8751db6

Convergence concepts and the Weak Law of Large Numbers (for uncorrelated r.v.'s)

Elementary "conditional probability" (and Bayes' rule, etc.) from HVG's cond_probTheory

Cumulative fixes according to review comments

Radon-Nikodym Theorem for [0,+Inf]-Measure Theory (HVG concordia)

Borel and Lebesgue measure spaces (and their equivalence on Borel sets)

Fixed real_topologyTheory for tight equality

Re-defined ext_suminf (extrealTheory), only specified for positive functions;
Stop generating HTML files for probability scripts.

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`.

Fix src/probability for tight equality

Remove TABs from src

Will also make selftest to check that they aren't introduced

Previous additions in probabilityTheory is useful only for prob_algebraScript.sml, move out.

Added some extra theorems from version 2 of probabilityTheory

Merged more countable theorems into pred_setTheory

Use standard (>>, >-, >|) symbolic connectives for THEN*

This is done under src/, replacing Joe Hurd's earlier versions of the
same which were ++, >> and << respectively. His proofs also
occasionally rely on the fact that he made >> and >|
right-associative, which is a great idea. His symbols are inherently
bad but they clash with existing practice, and there seems to be a
good argument to trying to keep material in src reasonably
consistent. (Using >> for THEN1 instead of THEN is particularly
confusing given our current practice.)

Fix probability theories in light of pat_assum rename

make non-script files in src/ non-executable

added finite_support_expectation

Delete trailing whitespace in src/

Integral on extended-real numbers [-Inf, +Inf]

Delete trailing whitespace in src/

modified prob theories according to #69

Remove src/probability's redundant def'ns of THEN1 and REVERSE.

Delete src/probability's copy of BIGINTER constant; use standard one.

Updated files for version in repository

Start of work to incorporate Concordia probability theory.

Added Probability Theory