Split `probability.v` into a directory `probability_theory`

[affeldt-aist]

Anticipating PRs of results from PR #1645 ("Bernoulli sampling", fyi: @hoheinzollern @t6s @proux01 @CohenCyril ) and PR #1391 (about independence of RVs, fyi: @hoheinzollern @t6s )

1. review and merge Add lemma pmf_measurable #1827 @Yosuke-Ito-345
2. split probability.vsplit probability.v #1842
3. a. rebase and review/merge PR independence, expectation of product #1391
4. b. PR power_measure from PR [Paper Artifact] Bernoulli sampling theorem #1645 (and maybe before that minor things at the top of the main file of this PR)

[Yosuke-Ito-345]

After the pull request #1827 is merged, I will send the next pull request which includes

Let mu : {measure set _ -> \bar R} := @lebesgue_measure R.

Lemma lebesgue_measure_oppr A (mA : measurable A) :
  pushforward(T2 := measurableTypeR R) mu -%R A = mu A.

Lemma ge0_integral_oppr (f : R -> \bar R)
  (mf : measurable_fun setT f) (ge0 : forall r, 0 <= f r) :
  \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R.

Lemma lebesgue_integral_pmf :
  \int[lebesgue_measure]_r (pmf X r)%:E = 0.

Lemma cdf_measurable : measurable_fun setT (cdf X).

Lemma ccdf_measurable : measurable_fun setT (ccdf X).

Lemma ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R ->
  'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P [set x | (r <= X x)%R].

Lemma le0_expectation_cdf (X : {RV P >-> R}) : (forall x, X x <= 0)%R ->
  'E_P[X] = - \int[mu]_(r in `]-oo, 0%R]) cdf X r.

These lemmas are now formally proved.
If you need one of these lemmas, please let me know.

[affeldt-aist]

The ones that do not depend on probability.v can maybe be PRed already.