notation in probability theory

Stream: general

[Jason KY.]

For measure theory, we have in general used α for the underlying type of a measurable space and μ for a measure on α. Right now in the probability folder, most files continue to use this notation except for the strong_law file where the standard probability notations are used (i.e.Ω for the type and ℙ is the measure) . @Sebastien Gouezel said in #14933 that using the probability notation will help more probability-inclined readers and I agree also. Should we change the notations in the probability folder to the probability notations?
(cc. @Kalle Kytölä who also had opinions on this)

[Jason KY.]

/poll Change to probability notations?
Yes
No

[Jason KY.]

(Note that ℙ will not be a probability measure most of the time but a finite measure since a surprising amount of probability theorems remains to hold)

[Kalle Kytölä]

I think notational cues are quite important for readability!

Without a doubt, one will face some tough calls about what is probability theory and what is measure theory... But even X for the space (pretty neutral in measure theory, right?) is better than α (one never encounters α in this role in math texts).

[Kalle Kytölä]

Another question is if we should actively change the existing conventions or take the more passive approach that in new additions we prefer better mathematical cues in the notation.... I don't have strong opinions about that, but if there is a reasonable consensus and someone is willing to improve the notation, then I'm obviously happy!

(In the weak convergence file I have been planning to switch to either measure theory X or probability theory Ω at some point, but somehow started and got stuck with the mathlib's generic (α : Type*)...).

[Jason KY.]

I personally prefer consistency over whatever notations we choose so I think it's a good idea to change the notations to the older files to be consistent with whatever decision we decide to make (it will be a simple search and replace also so it's not too much work :))