Mathlib.Probability

The standard normal CDF Φ is continuous: the standard normal has no atoms.

For any real score x, applying the probit transform to Φ(x) recovers x: the probit function Φ⁻¹ is a left inverse of the standard normal CDF Φ.

Let $p$ be a Bernoulli success probability with $0 \le p \le 1$, and let $q$ be a reference success probability with $0 < q < 1$. Then the Kullback–Leibler divergence from the Bernoulli($p$) law to the Bernoulli($q$) law equals $p \log(p/q) + (1-p)\log((1-p)/(1-q))$, the usual two-point KL formula: a success contribution plus a failure contribution.

If both success probabilities $p$ and $q$ lie in the middle half of the unit interval, $1/4 \le p \le 3/4$ and $1/4 \le q \le 3/4$, then the Kullback–Leibler divergence from the Bernoulli($p$) law to the Bernoulli($q$) law is at most four times the squared difference of the probabilities, $4(p-q)^2$.

Deterministic-scalar Slutsky theorem for random variables. If a sequence of random variables X n converges in distribution to Z, all under the same probability measure μ and a sequence of deterministic real scalars a n converges to a limit a₀, then the scaled sequence a n · X n converges in distribution to a₀ · Z.

Measure-level deterministic-scalar Slutsky theorem for weak convergence. For a filter l along which a family of probability measures on the reals converges weakly to a limit measure ν and a family of real scalars converges to a limit a₀, then the pushforwards of the measures by scalar multiplication x ↦ aᵢ·x converge weakly to the pushforward of ν by x ↦ a₀·x.

Cauchy–Schwarz for covariance. Under a finite measure, if $X$ is square-integrable and $Y$ is square-integrable, then the absolute value of their covariance is at most the product of their standard deviations, $|\mathrm{Cov}(X,Y)| \le \sqrt{\mathrm{Var}(X)} \cdot \sqrt{\mathrm{Var}(Y)}$.

For two probability laws, a measurable event, and two square-integrable branch functions, the selected function's variance is the mixture of branch variances plus the between-branch mean term.

For a finite index type ι, a measure μ, a measurable set A, measurable cells C that are pairwise disjoint, cover the space, and whose intersections with A have finite mass, and an integrable function f on a measurable space, the mass-ratio cell decomposition holds.

For a measurable positive-mass cell, measurable finite-coordinate random vectors, integrable individual coordinates, and factorization of every bounded measurable test under the normalized cell law, the complete normalized cross-moment matrix is the outer product of the two normalized first-moment vectors.

Given a finite stochastic matrix, a nonnegative contraction coefficient, half-ℓ¹ contraction of its forward action, an initial oscillation bound, and a number of steps, the iterated backward operator's oscillation is bounded by the coefficient raised to the number of steps times the initial bound, which decays geometrically when the coefficient is below one.

For two stochastic transition matrices, two probability initial laws, a unit-range reference reward, an initial-law total-variation error, a uniform row total-variation error, a uniform reward error, and a horizon, the finite-horizon moments differ by at most the sum of the initial, accumulated transition, and reward errors.

Given a probability measure, a finite collection of cells, measurability of every cell, pairwise disjointness of distinct cells, coverage of the whole sample space, an event, measurability of that event, a probability bound, and that bound conditional on each positive-mass cell, the unconditional event probability is at most the same bound.

Gaussian survival. For a normal law with mean m and a nonnegative variance parameter v that is nonzero, the probability mass above a threshold c equals one minus the standard-normal CDF evaluated at the standardized threshold (c − m)/√v.

Gaussian truncated first moment. For a normal law with mean m and a nonnegative variance parameter v that is nonzero, the first moment integrated over the tail above a threshold c equals m·(1 − Φ(t)) + √v·φ(t), where t = (c − m)/√v — the affine image of the standard-normal truncated moment ∫_{t}^∞ z φ(z) dz = φ(t).

A weighted sum of independent standard Gaussians with fixed weights has the centred Gaussian law whose variance is the sum of the squared weights, provided the family is mutually independent, each variable is measurable, and each has the standard Gaussian law.

Probabilists' Hermite polynomials satisfy the real exponential generating series, Gaussian orthogonality with factorial norms, and the zero-order identity.