mathlib3

a150b69f - chore(probability/*): change to probability notation in the probability folder (#15933)

chore(probability/*): change to probability notation in the probability folder (#15933) This PR makes two notational changes in the probability folder: `α` changed to `Ω` and `x` of type `α` to `ω`.