Measurability, reciprocal bounds, and ratio asymptotics of the 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.

The reciprocal (Real.Gamma s)⁻¹, on the other hand, is continuous on all of ℝ: Mathlib's convention Real.Gamma (-n) = 0 makes it vanish at the poles, matching the zeros of the entire function 1 / Γ. It is bounded on every half-line [a, ∞), which is what uniform estimates for series with coefficients 1 / Γ(b + n), such as hypergeometric and Bessel series, need. For a complex parameter the corresponding estimate is the factorial decay of 1 / Γ(s + n) on the half-plane 1 ≤ Re s.

Finally, the rising factorial is recorded as a quotient of real Gamma values, and Mathlib's Euler limit formula Real.GammaSeq_tendsto_Gamma is recast as the asymptotic equivalence Γ(n + 1 + s) ~ n ^ s * n! along the natural numbers, valid for every real shift s. This is the form in which polynomial decay of Gamma quotients such as Γ(n + a) / Γ(n + b) enters summability and moment arguments for discrete laws with Beta-function masses.

Main results

• Real.measurable_Gamma — Real.Gamma is measurable.
• Real.continuous_inv_Gamma — s ↦ (Real.Gamma s)⁻¹ is continuous.
• TauCeti.continuous_Gamma_sum_div_prod — the finite Gamma quotient is jointly continuous on positive parameters.
• Real.exists_abs_inv_Gamma_le — (Real.Gamma s)⁻¹ is bounded on [a, ∞).
• Real.Gamma_add_nat_div_Gamma_eq — Γ(x + n) / Γ x is the rising factorial x (x + 1) ⋯.
• Real.prod_range_add_mul_Gamma — s (s + 1) ⋯ (s + n - 1) Γ s = Γ(s + n) for positive s.
• Real.Gamma_nat_add_half_eq_factorial — Γ(n + 1 / 2) = (2 n)! √π / (4 ^ n n!).
• Real.isEquivalent_Gamma_natCast_add_one_add — Γ(n + 1 + s) ~ n ^ s * n! as n → ∞.
• Real.tendsto_Gamma_natCast_add_div_Gamma_natCast_add_atTop — Γ(n + a) / Γ(n + b) → 0 for a < b.
• Complex.norm_inv_Gamma_add_natCast_le — ‖1 / Γ(s + k)‖ ≤ ‖1 / Γ(s)‖ / k! for 1 ≤ Re s, the complex counterpart of the half-line bound used for series with coefficients 1 / Γ(b + k).
• Complex.sum_range_neg_one_pow_div_factorial_mul_Gamma — the alternating sum ∑_{i ≤ m} (−1)ⁱ / (i! Γ(a + m − i + 1)) = (−1)ᵐ / (m! (a + m) Γ(a)) for a ∉ −ℕ.

theorem Real.measurable_Gamma : Measurable Gamma

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

theorem Real.continuous_inv_Gamma : Continuous fun (s : ℝ) => (Gamma s)⁻¹

The reciprocal of the real Gamma function is continuous on all of ℝ, including at the poles of Real.Gamma, where both it and the entire function 1 / Γ vanish.

theorem TauCeti.continuous_Gamma_sum_div_prod {ι : Type u_1} [Fintype ι] : Continuous fun (a : ι → ↑(Set.Ioi 0)) => Real.Gamma (∑ i : ι, ↑(a i)) / ∏ i : ι, Real.Gamma ↑(a i)

For a finite family of positive parameters, the Gamma quotient Γ(∑ i, a i) / ∏ i, Γ(a i) is jointly continuous.

theorem Real.exists_abs_inv_Gamma_le (a : ℝ) : ∃ (C : ℝ), ∀ (s : ℝ), a ≤ s → |(Gamma s)⁻¹| ≤ C

The reciprocal of the real Gamma function is bounded on every half-line [a, ∞).

theorem Real.Gamma_add_nat_div_Gamma_eq {n : ℕ} (x : ℝ) (hx : ∀ (k : ℕ), x ≠ -↑k) : Gamma (x + ↑n) / Gamma x = Polynomial.eval x (ascPochhammer ℝ n)

The ascending Pochhammer symbol is given by the ratio of real Γ values; this is the real counterpart of Complex.Gamma_add_nat_div_Gamma_eq.

theorem Real.prod_range_add_mul_Gamma {s : ℝ} (hs : 0 < s) (n : ℕ) : (∏ j ∈ Finset.range n, (s + ↑j)) * Gamma s = Gamma (s + ↑n)

The product s (s + 1) ⋯ (s + n - 1) times Γ s is Γ (s + n), for positive s.

theorem Real.Gamma_nat_add_half_eq_factorial (n : ℕ) : Gamma (↑n + 1 / 2) = ↑(2 * n).factorial * √Real.pi / (4 ^ n * ↑n.factorial)

The half-integer value Γ(n + 1 / 2) = (2 n)! √π / (4 ^ n n!), the factorial form of Real.Gamma_nat_add_half, obtained from Legendre's duplication formula at n + 1 / 2.

theorem Real.isEquivalent_Gamma_natCast_add_one_add (s : ℝ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => Gamma (↑n + 1 + s)) fun (n : ℕ) => ↑n ^ s * ↑n.factorial

Euler's limit formula in ratio form. For every real s, Γ(n + 1 + s) is asymptotic to n ^ s * n! as the natural number n tends to infinity.

theorem Real.tendsto_Gamma_natCast_add_div_Gamma_natCast_add_atTop {a b : ℝ} (hab : a < b) : Filter.Tendsto (fun (n : ℕ) => Gamma (↑n + a) / Gamma (↑n + b)) Filter.atTop (nhds 0)

The Gamma quotients Γ(n + a) / Γ(n + b) tend to zero along the natural numbers when a < b, since they decay like n ^ (a - b).

theorem Complex.norm_inv_Gamma_add_natCast_le {s : ℂ} (hs : 1 ≤ s.re) (k : ℕ) : ‖(Gamma (s + ↑k))⁻¹‖ ≤ ‖(Gamma s)⁻¹‖ / ↑k.factorial

On the half-plane 1 ≤ Re s, the reciprocal Gamma function decays factorially along s + k: ‖1 / Γ(s + k)‖ ≤ ‖1 / Γ(s)‖ / k!. Together with the boundedness of 1 / Γ on compact sets, this gives locally uniform bounds for series with coefficients 1 / Γ(b + k) as functions of a complex parameter b.

theorem Complex.sum_range_neg_one_pow_div_factorial_mul_Gamma {a : ℂ} (ha : ∀ (n : ℕ), a ≠ -↑n) (m : ℕ) : ∑ i ∈ Finset.range (m + 1), (-1) ^ i / (↑i.factorial * Gamma (a + ↑(m - i) + 1)) = (-1) ^ m / (↑m.factorial * (a + ↑m)) * (Gamma a)⁻¹

A finite alternating sum of reciprocal Gamma values: for a ∉ −ℕ, ∑_{i ≤ m} (−1)ⁱ / (i! Γ(a + m − i + 1)) = (−1)ᵐ / (m! (a + m) Γ(a)). This is the coefficient identity behind the expansion of Tricomi's incomplete Gamma function in powers of −z (DLMF 8.7.1).