The lower incomplete gamma function

For a positive shape parameter s this file introduces

• TauCeti.lowerIncompleteGamma s x = ∫ t in 0..x, t ^ (s - 1) * exp (-t), the truncation of Euler's integral at x, extended by 0 for x ≤ 0 and for s ≤ 0; and
• TauCeti.regularizedGamma s x = lowerIncompleteGamma s x / Real.Gamma s, its normalization, again extended by 0 for s ≤ 0.

Classically these are γ(s, x) and P(s, x). The regularized function is the cumulative distribution function of a Gamma law, which is where this file is headed; the two totalizations above make that cdf agree with the clamping conventions a cdf needs, below the support and outside the parameter range.

Main definitions

• TauCeti.lowerIncompleteGamma — the lower incomplete gamma function γ(s, x);
• TauCeti.regularizedGamma — the regularized lower incomplete gamma function P(s, x).

Main results

• TauCeti.lowerIncompleteGamma_eq_integral and TauCeti.regularizedGamma_eq_div — the characteristic descriptions replacing the clamped definitions;
• TauCeti.intervalIntegrable_rpow_mul_exp_neg — convergence of Euler's integrand on an interval, including at the singularity 0 for s < 1;
• TauCeti.continuous_lowerIncompleteGamma, TauCeti.continuous_regularizedGamma — continuity on all of ℝ, in particular at x = 0, where for s < 1 the integrand blows up;
• TauCeti.lowerIncompleteGamma_monotone, TauCeti.regularizedGamma_monotone — monotonicity, and TauCeti.lowerIncompleteGamma_nonneg, TauCeti.regularizedGamma_nonneg, TauCeti.regularizedGamma_le_one — the range;
• TauCeti.hasDerivAt_lowerIncompleteGamma, TauCeti.hasDerivAt_regularizedGamma and the companion deriv lemmas — differentiability, for 0 < x only;
• TauCeti.lowerIncompleteGamma_add_one and TauCeti.regularizedGamma_add_one — the recurrence γ(s + 1, x) = s * γ(s, x) - x ^ s * exp (-x) and its regularized form P(s + 1, x) = P(s, x) - x ^ s * exp (-x) / Γ(s + 1), both for 0 < s and 0 ≤ x;
• TauCeti.tendsto_lowerIncompleteGamma_atTop, TauCeti.tendsto_regularizedGamma_atTop — the limits Real.Gamma s and 1 as x → ∞, with the resulting bounds TauCeti.lowerIncompleteGamma_le_Gamma and TauCeti.regularizedGamma_le_one;
• TauCeti.regularizedGamma_one — P(1, x) = 1 - e ^ (-x) for 0 ≤ x, the exponential cdf.
• TauCeti.Real.erf_eq_regularizedGamma_half_sq — the error function is the regularized incomplete gamma function of shape 1 / 2 after squaring, on the nonnegative half-line.

Implementation

The guard 0 < s in the definition of regularizedGamma mirrors the one built into TauCeti.lowerIncompleteGamma, which is the definition shape the roadmap prescribes. It changes no value: γ(s, x) already vanishes for s ≤ 0, so dividing unconditionally would give the same function, and TauCeti.regularizedGamma_eq_div accordingly needs no hypothesis on s.

The limit at infinity is Mathlib's Real.GammaIntegral_convergent together with Real.Gamma_eq_integral, which state Euler's integrand as exp (-t) * t ^ (s - 1); this file uses the opposite factor order throughout, so both are applied up to mul_comm at their point of use.

The recurrence is obtained from Mathlib's Complex.partialGamma_add_one, whose proof performs the integration by parts on Set.Ioo 0 x — the endpoint 0 has to be avoided because t ^ s is not differentiable there for s < 1. The bridge is TauCeti.ofReal_lowerIncompleteGamma_eq_partialGamma, which identifies γ(s, x) with Complex.partialGamma s x for real s.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 2, the "Lower incomplete gamma" target.
• NIST Digital Library of Mathematical Functions, ch. 8, especially §8.2 for incomplete gamma functions and Eq. 8.4.1 for their relation with the error function.

Convergence of the truncated Euler integral

theorem TauCeti.intervalIntegrable_rpow_mul_exp_neg {p : ℝ} (hp : -1 < p) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => t ^ p * Real.exp (-t)) MeasureTheory.volume a b

Euler's integrand t ^ p * exp (-t) is interval integrable, for -1 < p.

This composes Mathlib's intervalIntegral.intervalIntegrable_rpow', which carries the singularity at 0 for p < 0, with the continuous factor. The shape parameter s of TauCeti.lowerIncompleteGamma enters as p = s - 1.

The definitions

noncomputable def TauCeti.lowerIncompleteGamma (s x : ℝ) : ℝ

The lower incomplete gamma function γ(s, x) = ∫ t in 0..x, t ^ (s - 1) * exp (-t).

It is 0 for x ≤ 0, where the truncated integral is empty, and 0 for s ≤ 0, where Euler's integral diverges at the origin.

Equations

• TauCeti.lowerIncompleteGamma s x = if 0 < s then ∫ (t : ℝ) in 0..max x 0, t ^ (s - 1) * Real.exp (-t) else 0

noncomputable def TauCeti.regularizedGamma (s x : ℝ) : ℝ

The regularized lower incomplete gamma function P(s, x) = γ(s, x) / Γ(s), extended by 0 outside the valid range 0 < s of the shape parameter.

Equations

• TauCeti.regularizedGamma s x = if 0 < s then TauCeti.lowerIncompleteGamma s x / Real.Gamma s else 0

theorem TauCeti.lowerIncompleteGamma_eq_integral {s x : ℝ} (hs : 0 < s) (hx : 0 ≤ x) : lowerIncompleteGamma s x = ∫ (t : ℝ) in 0..x, t ^ (s - 1) * Real.exp (-t)

In the valid range, γ(s, x) is the truncated Euler integral.

@[simp]

theorem TauCeti.lowerIncompleteGamma_eq_zero_of_nonpos_left {s : ℝ} (hs : s ≤ 0) (x : ℝ) : lowerIncompleteGamma s x = 0

Outside the valid range of the shape parameter, γ(s, x) is 0.

@[simp]

theorem TauCeti.lowerIncompleteGamma_eq_zero_of_nonpos_right {x : ℝ} (s : ℝ) (hx : x ≤ 0) : lowerIncompleteGamma s x = 0

Below the support, γ(s, x) is 0.

@[simp]

theorem TauCeti.regularizedGamma_eq_zero_of_nonpos_left {s : ℝ} (hs : s ≤ 0) (x : ℝ) : regularizedGamma s x = 0

Outside the valid range of the shape parameter, P(s, x) is 0.

theorem TauCeti.regularizedGamma_eq_div (s x : ℝ) : regularizedGamma s x = lowerIncompleteGamma s x / Real.Gamma s

P(s, x) is γ(s, x) normalized by Γ(s).

No hypothesis on the shape parameter is needed: for s ≤ 0 both sides are 0, since γ(s, ·) is.

@[simp]

theorem TauCeti.regularizedGamma_eq_zero_of_nonpos_right {x : ℝ} (s : ℝ) (hx : x ≤ 0) : regularizedGamma s x = 0

Below the support, P(s, x) is 0.

Positivity, monotonicity and regularity

theorem TauCeti.lowerIncompleteGamma_nonneg (s x : ℝ) : 0 ≤ lowerIncompleteGamma s x

γ(s, x) is nonnegative, for every parameter value.

theorem TauCeti.regularizedGamma_nonneg (s x : ℝ) : 0 ≤ regularizedGamma s x

P(s, x) is nonnegative, for every parameter value.

theorem TauCeti.lowerIncompleteGamma_monotone (s : ℝ) : Monotone (lowerIncompleteGamma s)

γ(s, ·) is monotone: it accumulates a nonnegative integrand.

theorem TauCeti.regularizedGamma_monotone (s : ℝ) : Monotone (regularizedGamma s)

P(s, ·) is monotone. For 0 < s, this together with TauCeti.regularizedGamma_nonneg, TauCeti.regularizedGamma_le_one, TauCeti.regularizedGamma_eq_zero_of_nonpos_right, TauCeti.continuous_regularizedGamma and TauCeti.tendsto_regularizedGamma_atTop is everything a cumulative distribution function must satisfy.

theorem TauCeti.continuous_lowerIncompleteGamma (s : ℝ) : Continuous (lowerIncompleteGamma s)

γ(s, ·) is continuous on all of ℝ.

For s < 1 this includes the point x = 0, where the integrand is unbounded; the integral is nevertheless convergent there, by TauCeti.intervalIntegrable_rpow_mul_exp_neg.

theorem TauCeti.continuous_regularizedGamma (s : ℝ) : Continuous (regularizedGamma s)

P(s, ·) is continuous on all of ℝ.

theorem TauCeti.hasDerivAt_lowerIncompleteGamma {s x : ℝ} (hs : 0 < s) (hx : 0 < x) : HasDerivAt (lowerIncompleteGamma s) (x ^ (s - 1) * Real.exp (-x)) x

γ(s, ·) is differentiable at every positive x, with the expected derivative.

The hypothesis 0 < x cannot be weakened to 0 ≤ x: among the positive shapes this theorem is stated for, differentiability at 0 holds exactly for 1 < s. For s < 1 the integrand is unbounded at 0, and at s = 1 the clamped function is x ↦ 1 - exp (-max x 0), whose one-sided derivatives at 0 are 0 and 1. (For s ≤ 0 the function is identically 0, hence trivially differentiable everywhere.)

theorem TauCeti.deriv_lowerIncompleteGamma {s x : ℝ} (hs : 0 < s) (hx : 0 < x) : deriv (lowerIncompleteGamma s) x = x ^ (s - 1) * Real.exp (-x)

The derivative of γ(s, ·) at a positive point is the integrand.

theorem TauCeti.hasDerivAt_regularizedGamma {s x : ℝ} (hs : 0 < s) (hx : 0 < x) : HasDerivAt (regularizedGamma s) (x ^ (s - 1) * Real.exp (-x) / Real.Gamma s) x

P(s, ·) is differentiable at every positive x, with the expected derivative. As for TauCeti.hasDerivAt_lowerIncompleteGamma, the hypothesis 0 < x is needed at every shape 0 < s ≤ 1.

theorem TauCeti.deriv_regularizedGamma {s x : ℝ} (hs : 0 < s) (hx : 0 < x) : deriv (regularizedGamma s) x = x ^ (s - 1) * Real.exp (-x) / Real.Gamma s

The derivative of P(s, ·) at a positive point is the normalized integrand.

The recurrence in the shape parameter

theorem TauCeti.ofReal_lowerIncompleteGamma_eq_partialGamma {s x : ℝ} (hs : 0 < s) (hx : 0 ≤ x) : ↑(lowerIncompleteGamma s x) = (↑s).partialGamma x

For a positive real shape parameter s and 0 ≤ x, γ(s, x) is Mathlib's Complex.partialGamma at (s : ℂ).

The complex partial gamma function carries the integration by parts behind TauCeti.lowerIncompleteGamma_add_one, so this identification is what lets that recurrence be imported rather than reproved.

theorem TauCeti.lowerIncompleteGamma_add_one {s x : ℝ} (hs : 0 < s) (hx : 0 ≤ x) : lowerIncompleteGamma (s + 1) x = s * lowerIncompleteGamma s x - x ^ s * Real.exp (-x)

The recurrence γ(s + 1, x) = s * γ(s, x) - x ^ s * exp (-x), for 0 < s and 0 ≤ x.

theorem TauCeti.regularizedGamma_add_one {s x : ℝ} (hs : 0 < s) (hx : 0 ≤ x) : regularizedGamma (s + 1) x = regularizedGamma s x - x ^ s * Real.exp (-x) / Real.Gamma (s + 1)

The regularized form of the recurrence, P(s + 1, x) = P(s, x) - x ^ s * exp (-x) / Γ(s + 1), for 0 < s and 0 ≤ x. The factor s of TauCeti.lowerIncompleteGamma_add_one is absorbed by Real.Gamma_add_one.

The limit at infinity

theorem TauCeti.tendsto_lowerIncompleteGamma_atTop {s : ℝ} (hs : 0 < s) : Filter.Tendsto (lowerIncompleteGamma s) Filter.atTop (nhds (Real.Gamma s))

γ(s, x) increases to the complete Euler integral Real.Gamma s as x → ∞.

theorem TauCeti.lowerIncompleteGamma_le_Gamma {s : ℝ} (hs : 0 < s) (x : ℝ) : lowerIncompleteGamma s x ≤ Real.Gamma s

A truncated Euler integral is at most the complete one.

theorem TauCeti.tendsto_regularizedGamma_atTop {s : ℝ} (hs : 0 < s) : Filter.Tendsto (regularizedGamma s) Filter.atTop (nhds 1)

P(s, x) increases to 1 as x → ∞: it is the cumulative distribution function of a probability law.

theorem TauCeti.regularizedGamma_le_one (s x : ℝ) : regularizedGamma s x ≤ 1

P(s, x) is at most 1, for every parameter value.

The exponential case s = 1

@[simp]

theorem TauCeti.lowerIncompleteGamma_one {x : ℝ} (hx : 0 ≤ x) : lowerIncompleteGamma 1 x = 1 - Real.exp (-x)

γ(1, x) = 1 - exp (-x) for 0 ≤ x.

@[simp]

theorem TauCeti.regularizedGamma_one {x : ℝ} (hx : 0 ≤ x) : regularizedGamma 1 x = 1 - Real.exp (-x)

P(1, x) = 1 - exp (-x) for 0 ≤ x: the regularized lower incomplete gamma function at shape 1 is the cumulative distribution function of the standard exponential law.

Relation with the error function

theorem TauCeti.hasDerivAt_regularizedGamma_half_sq {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (y : ℝ) => regularizedGamma (1 / 2) (y ^ 2)) (2 / √Real.pi * Real.exp (-x ^ 2)) x

On the positive half-line, the regularized incomplete gamma function of shape 1 / 2, composed with squaring, has the Gaussian derivative which defines the error function.

theorem TauCeti.Real.erf_eq_regularizedGamma_half_sq {x : ℝ} (hx : 0 ≤ x) : erf x = regularizedGamma (1 / 2) (x ^ 2)

For 0 ≤ x, the error function is the regularized lower incomplete gamma function of shape 1 / 2 evaluated at x². The restriction is necessary because the right-hand side is even, whereas the error function is odd.