Measurability of the real Gamma function

Real.Gamma is smooth away from the nonpositive integers and has a pole at each of them, so it is neither continuous nor locally bounded on all of ℝ. It is nevertheless Borel measurable, because the set of its singularities is countable.

Mathlib records the analytic side of this (Real.differentiableAt_Gamma, Real.not_continuousAt_Gamma_neg_nat) but never draws the measurability conclusion. It is needed as soon as a formula containing Real.Gamma s is integrated or measured in the variable s — for instance for the normalizing constants of the Gamma and Beta densities, which is why their family-specific measurability modules use this result.

Main results

• Real.measurable_Gamma — Real.Gamma is measurable.

theorem Real.measurable_Gamma : Measurable Gamma

The real Gamma function is Borel measurable on all of ℝ, including at its poles.