Quantile function

The quantile function or (generalized) inverse distribution function of a real random variable with cumulative distribution function is defined as #m/def/prob

and is thus a left inverse of .

Proof of left-inverse

Note that since is monotone increasing, implies , so

as required.

#state/tidy | #lang/en | #SemBr