Infinite-dimensional Borel space

[binghe]

Hi,

This PR adds the formalisation of infinite-dimensional Borel space (Borel_inf) [1, p.178-179], another important part for the general theory of stochastic processes. One of its alternative definitions depends on the list-based n-dimensional Borel spaces (#1288), committed days ago.

Here a "point" of infinite dimensional space is an infinite (countable) sequence of extended reals (extreal), represented by a function of type :num -> extreal. A "cylinder" in this space is a set of such points such that the first N dimension forms a rectangle (while other dimensions range over all possible values, i.e. no requirements at all):

[cylinder_def] (stochastic_processTheory)
⊢ ∀h N. cylinder h N = {f | ∀n. n < N ⇒ f n ∈ h n}

A cylinder can be cut off to first N dimensions, to form a rectangle (see #1288 for its definition). This operation is a function called cylinder2rect:

[cylinder2rect_def]
⊢ ∀c N. cylinder2rect c N = IMAGE (λf. GENLIST f N) c

Furthermore, note that the type of "cylinder" is :(num -> α) -> bool (a set of num -> 'a functions), but not every term of this type is a valid cylinder. The following predicate is_cylinder can be used to test if it's really a cylinder:

[is_cylinder_def]
⊢ ∀c N. is_cylinder c N ⇔ c = ∅ ∨ ∀f. GENLIST f N ∈ cylinder2rect c N ⇒ f ∈ c

Now there are 3 different ways to define this Borel_inf, based the previous defined Borel_lists and the above new cylinder concepts:

[Borel_inf_def]
⊢ Borel_inf =
  sigma 𝕌(:num -> extreal)
    {cylinder h N | 0 < N ∧ ∀i. i < N ⇒ ∃c. h i = {x | x ≤ c}}

[Borel_inf1_def]
⊢ Borel_inf1 =
  sigma 𝕌(:num -> extreal)
    {cylinder h N | 0 < N ∧ ∀i. i < N ⇒ h i ∈ subsets Borel}

[Borel_inf2_def]
⊢ Borel_inf2 =
  sigma 𝕌(:num -> extreal)
    {c |
     (∃N. 0 < N ∧ is_cylinder c N ∧
          cylinder2rect c N ∈ subsets (Borel_lists N))}

It turns out that the above 3 definitions are equivalent: (thus in proofs using them one can choose the more appropriate one to use)

[Borel_inf_eq_Borel_inf1]
⊢ Borel_inf = Borel_inf1

[Borel_inf_eq_Borel_inf2]
⊢ Borel_inf = Borel_inf2

The most difficult part of this work is the following theorem (with 500 lines of proof) about the alternative definition (list-based) n-dimensional sigma-algebra by sigma-generators:

[sigma_lists_alt_generator]
⊢ ∀sp sts N.
    subset_class sp sts ∧ has_exhausting_sequence (sp,sts) ∧ 0 < N ⇒
    sigma_lists (sigma sp sts) N =
    sigma (rectangle (λn. sp) N) {rectangle h N | h | (∀i. i < N ⇒ h i ∈ sts)}

which requires a new fundamental theorem about the images of sigma generators:

   [IMAGE_SIGMA]  Theorem (sigma_algebraTheory)
      ⊢ ∀sp sts f.
          subset_class sp sts ∧ BIJ f sp (IMAGE f sp) ⇒
          IMAGE (IMAGE f) (subsets (sigma sp sts)) =
          subsets (sigma (IMAGE f sp) (IMAGE (IMAGE f) sts))

Other changes

In probabilityTheory I added the following theorem for fast constructing discrete probability spaces of with a household uniform distribution:

   [prob_space_on_finite_set]  Theorem (probabilityTheory)      
      ⊢ ∀p. FINITE (p_space p) ∧ p_space p ≠ ∅ ∧
            events p = POW (p_space p) ∧
            (∀s. s ∈ events p ⇒ prob p s = &CARD s / &CARD (p_space p)) ⇒
            prob_space p

[1] Shiryaev, A.N.: Probability-1. Springer-Verlag New York, New York, NY (2016).