Minor fix & updates to probability materials

[binghe]

Hi,

Here are some small updates, additions and fixes related to the probability-related material in HOL4, that I'd like to incorporate in the new release. Below is the list of changes following the shown order of file changes:

1. In examples/probability, I modified the Holmakefile to make sure the legacy material in the legacy subdirectory get built together.
2. In util_probTheory and then lebesgueTheory, the previous definition of disjoint_family (from HVG's work) can be simplified to an overload to disjoint_family_on:

   Overload disjoint_family = “\A. disjoint_family_on A UNIV”

3. Also in lebesgueTheory, the previous proof of integral_sum' has caused two HOL warnings saying "Type.mk_vartype: non-standard syntax". I don't understand this warning and I found the existing proof hard to understand. So I reworked this proof in my usual style (using the same lemmas as the old one).
4. In martingaleTheory, the following new lemma about "filtrations" of sigma-algebras is added (this is due to my other unfinished work):

   [filtration_from_measurable_functions]  Theorem
     ⊢ ∀m X A.
         measure_space m ∧
         (∀n. X n ∈ Borel_measurable (measurable_space m)) ∧
         (∀n. A n = sigma (m_space m) (λn. Borel) X (count1 n)) ⇒
         filtration (measurable_space m) A

5. In measureTheory, there was a definition sigma_finite_def0, previously renamed due to name conflicts. Now I have renamed them: sigma_finite_def0 to sigma_finite, and sigma_finite (a theorem) to sigma_finite_thm. The use of sigma_finite_thm is quite local, didn't cause too many modifications in other proofs.
6. In probabilityTheory, I added [nocompute] tag to the definition of converge_def. I don't think this converge definition needs to be put into computeLib (but the compilation outputs said so).

7. In sigma_algebraTheory, some new lemmas for sigma_functions has been added (This completes the semantics of sigma_functions, and is also due to my other unfinished work.), e.g.:

   [sigma_algebra_sigma_functions]  Theorem (sigma_algebraTheory)
     ⊢ ∀sp A f J.
         (∀i. f i ∈ (sp → space (A i))) ⇒ sigma_algebra (sigma sp A f J)
   
   [sigma_functions_subset]  Theorem
     ⊢ ∀A B f J.
         sigma_algebra A ∧ (∀i. i ∈ J ⇒ sigma_algebra (B i)) ∧
         (∀i. i ∈ J ⇒ f i ∈ measurable A (B i)) ⇒
         subsets (sigma (space A) B f J) ⊆ subsets A

8. In util_probTheory, beside the previous mentioned changes of disjoint_family, and some typesetting changes, I renamed one theorem to finite_disjoint_decomposition', to better match its nature.

9. In iterateTheory and also util_probTheory, I added two lemmas to connect COUNT (and its overloaded variant count1) with numseg:

   [COUNT_NUMSEG]  Theorem (iterateTheory)      
     ⊢ ∀n. 0 < n ⇒ count n = {0 .. n − 1}
   
   [count1_numseg]  Theorem (util_probTheory)
     ⊢ ∀n. count1 n = {0 .. n}

--Chun

[binghe]

There's also a fix of TeX munge outputs for NegInf (extreal_baseTheory); Added two lemmas in sigma_algebraTheory stating finite algebras are sigma-algebras.

[mn200]

Thanks for your work on this.