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.v
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)