Probabilistic convergence

[hoheinzollern]

Motivation for this change

Introduces probabilistic convergence

Things done/to do

• [ ] add weak law of large numbers
• [ ] prove Markov's and Chebyshev's inequality
• [ ] check proofs for probabilistic convergence

Co-authors: @affeldt-aist @t6s

[zstone1]

I'm very happy to see more specialized convergences. I will propose an alternate approach: to build a topology on {RV P >-> R} that induces this convergence. This is the approach I took for relating uniform, pointwise, and compact convergence on function spaces in topology.v, and I think it turned out pretty well.

The benefit of the approach is access to the wealth of general topology lemmas and notations. For example, you need a topology to even state that "expected value is continuous from {RV P >-> R} to R". The main downside of the approach is it takes extra effort, and sometimes the topologies are arcane (in this case it appears to be a simple metric, not too bad). I see three options A. Define the convergence as above, and prove it's backed by a topology B. Define the topology, and prove the above property as a lemma C. Not build underlying topology at all (you never actually need it to prove law of large numbers, CLT, etc).

To be concrete, wikipedia claims the metric d(x,y) := E(min(x => |X(x) - Y(x)|, 1) induces "convergence in probability". Also according to wikipedia, the "vague topology" should induce "convergence in distribution".

[zstone1]

As an aside, today I was quite surprised to learn that "almost everywhere convergence" is not topological. So while it looks like we could define a "filteredType" for it, we certainly cannot define a topologicalType for it.

[t6s]

As an aside, today I was quite surprised to learn that "almost everywhere convergence" is not topological. So while it looks like we could define a "filteredType" for it, we certainly cannot define a topologicalType for it.

The notion of convergence spaces might be useful? https://ncatlab.org/nlab/show/convergence+space

[affeldt-aist]

@hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the Section cvg_random_variable.

[affeldt-aist]

@hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the Section cvg_random_variable.

This might be still worth doing it, though after one year a copy-paste might be more effective than a rebase.