On the median of the beta distribution in relation to the median of the gamma distribution
Richard F. Lyon
math.ST
Oct 29, 2026 · v1
TL;DR
Most theorems on beta and gamma median bounds are machine-checked in Lean 4 with Mathlib, stated using Mathlib's gammaMeasure and betaMeasure CDFs.
Abstract
The median of the beta distribution has no closed form, but it is closely tied to the median of the gamma distribution. Kerman's approximation has the ratio form $g(α)/(g(α)+g(β))$ with $g(x) = x - 1/3$, a lower bound on the gamma median, and it is a lower bound on the beta median for $1/3 < α< β$. The ratio form built from the true gamma median is a tighter lower bound, asymptotically exact as $β\to \infty$. The ratio form built from the Wilson-Hilferty approximation to the gamma median, implicit in a classical approximation to the $F$ distribution but little known as an approximation to the beta median, is an upper bound on the edge $α= 1$ and for large shape parameters. The ratio form that is exact on the lines $α= 1$ and $β= 1$ yields a new approximation to the gamma median, which is an upper bound on it for shape parameter below 1 and a lower bound above 1; no ratio form gives the beta median exactly. For large shape parameters, the logit of the median has an explicit second-order expansion. For small shape parameters, bounds in elementary functions are asymptotically tight, and odds-corrected forms of the low-$α$ asymptote, with an elementary factor that is exact on the edges $α= 1$ and $β= 1$, are, numerically, one-sided bounds within 0.44% of the median that are exact on the lines $α= 1$, $β= 1$, and $α= β$. Steering their exponents with four fitted constants, and interpolating between two ratio forms where both shape parameters exceed 1, gives an approximation in elementary functions that is exact on those lines and numerically within 0.065% of the median over the whole domain. Most of the proofs are machine-verified in Lean 4.
Problem
The median of the beta distribution has no closed form. Existing approximations such as Kerman's ratio form lack rigorous bounding properties and accuracy over the whole parameter domain.
Approach
Ratio-form approximations g(α)/(g(α)+g(β)) are built from the gamma median and from approximations to it, including Wilson–Hilferty and a new form exact at α=1 and β=1. Low-α asymptotes with odds corrections are derived, and a combined elementary-function approximation uses fitted steering constants. Most proofs are formalized in Lean 4 with Mathlib, using Mathlib's probability distributions, and checked against the standard axioms.
Results
The ratio form built from the true gamma median is proved to be a tight lower bound on the beta median, asymptotically exact as β→∞. A new gamma median approximation log2/(2^{1/α}−1) is proved to be an upper bound for shape below 1 and a lower bound above 1. A combined elementary approximation is numerically within 0.065% of the beta median over the whole domain; several bounds remain conjectures or are verified only numerically.