mathlib documentation


Notations for probability theory #

This file defines the following notations, for functions X,Y, measures P, Q defined on a measurable space m0, and another measurable space structure m with hm : m ≤ m0,

TODO: define the notation ℙ s for the probability of a set s, and decide whether it should be a value in , ℝ≥0 or ℝ≥0∞.