A measurable space is a space equipped with a σ-algebra.

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

`X` has a sub-exponential moment generating function with parameters `(V, b)`: for every
`t` with `b * |t| ≤ 1`, `exp (t * X)` is integrable and `mgf X μ t ≤ exp (V * t ^ 2 / 2)`.
For `b = 0` this is `HasSubgaussianMGF X V μ`.

This is equivalent to `Kernel.HasSubexponentialMGF X V b (Kernel.const Unit μ) (Measure.dirac ())`,
as proved in `hasSubexponentialMGF_iff_kernel`.

A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function.

A similar notion is `MeasureTheory.NullMeasurable`. That notion is equivalent to `AEMeasurable` if
the σ-algebra on the codomain is countably generated, but weaker in general.