Analytic and optimized approximations to the median of the gamma distribution
Richard F. Lyon
math.ST
Nov 10, 2026 · v1
TL;DR
Theorems 1 and 2, bounds on the gamma median end functions, are machine-checked in Lean 4 with Mathlib; the Lean project is an arXiv ancillary file.
Abstract
The median $ν_Γ(α)$ of the gamma distribution has no closed form, but its behavior at both ends is known: it is asymptotic to $2^{-1/α}e^{-γ}$ (with $γ$ being the Euler-Mascheroni constant) as the shape parameter $α\to 0$, and approaches $α- 1/3$ as $α\to \infty$. We write approximations as interpolations $(1 - g)ν_0 + gν_\infty$ between two elementary-function bounds or approximations, each exact in one limit, with an interpolator $g(α)$ going from 0 to 1, and compare three such forms: a first one between previously proven bounds, a second ending in an approximation from the beta median that is exact at $α= 1$ but does not quite approach $α- 1/3$ as $α\to \infty$, and a third one, between bounds proved here, that corrects the large-$α$ end of the second. For each form, the ideal interpolator's slope at 0, approach to 1, and value at $α= 1$ are derived in closed form. Rational interpolators with every coefficient set in closed form from these properties, with no numerical fitting, reach a worst relative error of 0.0011 over all $α> 0$, with absolute error below 0.0002. Fitting some of these or other coefficients numerically to minimize the worst absolute-or-relative error then trades accuracy against complexity: the Pareto frontier reaches 0.000087 with two fitted constants and 0.000041 with five, and from two on uses degree-4 rationals of the second form with no $α^2$ term in the numerator. The proofs that the end functions of the first and third forms are bounds are machine-checked in Lean 4.
Problem
The median of the gamma distribution has no closed form. Its asymptotic behavior is known at both ends: 2^{-1/α}e^{-γ} as α→0 and α−1/3 as α→∞. Accurate elementary approximations valid for all α>0 are sought.
Approach
Approximations are written as interpolations (1−g)ν_0 + gν_∞ between two elementary end functions, each exact in one limit. Three such forms are compared, and new bounds are proved for the end functions of the third form. Rational interpolators have coefficients either set in closed form from properties of the ideal interpolator or fitted numerically. A Pareto frontier of worst absolute-or-relative error against the number of fitted constants is computed. The bound theorems are machine-checked in Lean 4 with Mathlib, building on an earlier formalization.
Results
Interpolators with all coefficients set in closed form reach a worst relative error of 0.0011 over all α>0. With numerical fitting, the worst error falls to 0.000087 with two fitted constants and 0.000041 with five. The proofs that the end functions are bounds are formally verified in Lean.
| n | Form A | Form B | Form C |
|---|
| 0 | 0.0131 | 0.00211 | 0.00111 |
| 1 | 0.00242 | 0.00186 | 0.000945 |
| 2 | 0.000177 | 0.000087 | 0.000158 |
| 5 | 0.000080 | 0.000041 | 0.000082 |
Best worst error by form and number of fitted constants n (selected rows)