[probability] add distributionTheory (former normal_rvTheory)

[binghe]

Hi,

This is in preparation of proving the Central Limit Theorem (a local student project). Previously (part of #1295) I added the concept of "convergence in distribution" for random variables ((X ⟶ Y) (in_distribution p)) but it turns out that the support of random variables taking potential infinite values is hard and not necessary (at this moment). The main difficulty is to prove that a continuous extreal-valued function is Borel-measurable. The related topology support (mostly the continuous map between two topspaces, from HOL-Light) is still missing.

So I decide to fallback to only support finite r.v.'s (i.e. real_random_variable) just like what I did initially for other convergence concepts. The new definition of "converge_in_dist" only involves "bounded and continuous" real-value functions (:real -> real), which is easier to handle:

   [converge_in_dist_def]  Theorem
      ⊢ ∀X Y p.
          (X ⟶ Y) (in_distribution p) ⇔
          ∀f. bounded (IMAGE f 𝕌(:real)) ∧ f continuous_on 𝕌(:real) ⇒
              ((λn. expectation p (Normal ∘ f ∘ real ∘ X n)) ⟶
               expectation p (Normal ∘ f ∘ real ∘ Y)) sequentially

Next we have the concepts of "weak convergence" of probability measures: A sequence of probability measures (of type :num -> extreal measure) is said to converge to another single one, if for all bounded and continuous (real-valued) functions, its integration w.r.t. probability measures converge to the integration of that single measure, as a converget sequence of extreal numbers:

[weak_converge_def]
⊢ ∀fi f.
    fi ⟶ f ⇔
    ∀g. bounded (IMAGE g 𝕌(:real)) ∧ g continuous_on 𝕌(:real) ⇒
        ((λn. ∫ (space Borel,subsets Borel,fi n) (Normal ∘ g ∘ real)) ⟶
         ∫ (space Borel,subsets Borel,f) (Normal ∘ g ∘ real)) sequentially

The connection between "convergence in distribution" and "weak convergence" is the following: convergence in distribution of r.v.'s is equivalent to the weak convergence of their distributions:

[converge_in_dist_alt]
⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (in_distribution p) ⇔
     (λn. distribution p (X n)) ⟶ distribution p Y)

And there's another form of the same connection theorem but in terms of explicit integrations:

[converge_in_dist_alt']
⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (in_distribution p) ⇔
     ∀f. bounded (IMAGE f 𝕌(:real)) ∧ f continuous_on 𝕌(:real) ⇒
         ((λn. expectation p (Normal ∘ f ∘ real ∘ X n)) ⟶
          expectation p (Normal ∘ f ∘ real ∘ Y)) sequentially)

Such a reduction from "convergence in distr." to "weak convergence" is usually the first step of proving Central Limit Theorems (CLTs).

The above theorems (and the definition of "weak convergence") are put into a new theory file distributionScript.sml under "examples/probability", which is renamed from "normal_rvScript.sml". I actually also ported a bit more work from HVG's old normal_rvTheory, e.g. the definition of "normal density", another piece of work needed for the proof of CLTs.

[normal_density]
⊢ ∀mu sig x.
    normal_density mu sig x =
    1 / sqrt (2 * pi * sig²) * exp (-(x − mu)² / (2 * sig²))

I plan to port more old code into this new distributionTheory.

Chun

[binghe]

I forgot to mention that, in pred_setTheory, the important theorem:

   [FINITE_is_measure_maximal]  Theorem      
      ⊢ ∀m s. FINITE s ∧ s ≠ ∅ ⇒ ∃x. is_measure_maximal m s x

previously had the free variable m instead of the universal quantifier. This has been proven to be very inconvenient (user has to do a GEN first). By adding the universal quantifier back, this creates a minor incompatibility issue, but the actual tests show just one broken theorem in the code base (more can be found in unknown user code). I think this change is in the right direction but I'm not sure if we need to mention it in the (next) release notes...

[mn200]

Thanks for your work on this!