Updates to convergence concepts for potential infinite-valued r.v.'s

[binghe]

Hi,

Currently the various convergence concepts for the sequences of random variables (r.v.'s) do not support r.v.'s taking infinite values (PosInf and NegInf), mostly because there was no way to express limits of extreal-valued functions when these concepts were first defined (#786, in 2020). Note that such limits didn't stop us from formalizing The Law of Large Numbers (#910, #938), where the involved r.v.'s are limited to "normal" extreals (real_random_variable).

My previous PR #993 in 2021 added a working canonical metric for extreals, and then #1111 added ext_tendsto for the limits of extreal-valued functions, based on the Moore-Smith covergence nets defined in real_topologyTheory. Finally we are ready to update the definitions of converge concepts using the limits of extreal-valued functions. For example, this is the old definition of "convergence almost everywhere", now becomes a theorem:

   [converge_AE_def]  Theorem (probabilityTheory)
      ⊢ ∀p X Y.
          (∀n. real_random_variable (X n) p) ∧ real_random_variable Y p ⇒
          ((X ⟶ Y) (almost_everywhere p) ⇔
           AE x::p. ((λn. real (X n x)) ⟶ real (Y x)) sequentially)

and this is the new definition: (Note the removal of real from the definition)

   [converge_AE]  Theorem      
      ⊢ ∀p X Y.
          (X ⟶ Y) (almost_everywhere p) ⇔
          AE x::p. ((λn. X n x) ⟶ Y x) sequentially

The new definition allows the convergence of r.v.'s to another r.v. taking infinities. E.g. in the following simple theorem, the variable c can be PosInf: (with the old definition, by real PosInf = 0, it will cause the wrong conclusion ((λx n. PosInf) ⟶ (λx. 0)) (almost_everywhere p))

   [converge_AE_const]  Theorem
      ⊢ ∀p c. prob_space p ⇒ ((λx n. c) ⟶ (λx. c)) (almost_everywhere p)

Similarly, the new definitions of convergence in pr. and convergence in L^p also become shorter and nicer:

   [converge_PR]  Theorem      
      ⊢ ∀p X Y.
          (X ⟶ Y) (in_probability p) ⇔
          ∀e. 0 < e ∧ e ≠ +∞ ⇒
              ((λn. prob p {x | x ∈ p_space p ∧ e < abs (X n x − Y x)}) ⟶ 0)
                sequentially

   [converge_LP]  Theorem      
      ⊢ ∀p X Y r.
          (X ⟶ Y) (in_lebesgue r p) ⇔
          (∀n. X n ∈ lp_space r p) ∧ Y ∈ lp_space r p ∧
          ((λn. expectation p (λx. abs (X n x − Y x) powr r)) ⟶ 0)
            sequentially

Furthermore, I did some preliminary work on the support of convergence in distribution (to support Central Limit Theorem in the future):

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

The above definition looks correct, but is not yet used/verified by any theorem. The involved bounded_on and continuous_on are newly defined in extrealTheory, also based on Moore-Smith nets from real_topologyTheory:

   [ext_continuous_def]  Definition      
      ⊢ ∀f net. f continuous net ⇔ (f ⟶ f (netlimit net)) net
   
   [ext_continuous_on_def]  Definition      
      ⊢ ∀f s. f continuous_on s ⇔ ∀x. x ∈ s ⇒ f continuous (at x within s)

   [bounded_on_def]  Definition      
      ⊢ ∀f s. f bounded_on s ⇔ ∃c. ∀x. x ∈ s ⇒ abs x ≤ Normal c

In real_topologyTheory, all basic theorems and definitions about the MR1 metrics and Moore-Smith nets are now moved to upstream in metricTheory and netsTheory, resp. This change only slightly shortened real_topologyScript.sml but greatly enriched metricTheory and netsTheory. (I plan to merge the old and new implementations of "nets" in netsTheory, in the future.) After the movements of these theorems, some probability scripts need to explicitly open metricTheory/netsTheory.

Finally, the Laws of large numbers (examples/probability/large_numberTheory) and related theorems using converge_AE and converge_PR are updated to work with their new definitions.

--Chun

[binghe]

Note also that, in topologyTheory, I ported a little from HOL-Light, the concept of "continuous map" between topological spaces:

   [continuous_map]  Definition      
      ⊢ ∀top top' f.
          continuous_map (top,top') f ⇔
          (∀x. x ∈ topspace top ⇒ f x ∈ topspace top') ∧
          ∀u. open_in top' u ⇒ open_in top {x | x ∈ topspace top ∧ f x ∈ u}

This is supposed to be equivalent with all kinds of continuous functions for reals and extreals, but so far the connections are not established yet. More work needs to be done here in the future.

[mn200]

Very nice!