Documentation

Mathlib.Probability.Notation

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,