Gamma distribution

TheoremIntegrability of the scaled gamma integrand#✓fully proved

For real numbers \(a > 0\) and \(s > 0\), the function \(x \mapsto x^{a-1} e^{-sx}\) is Lebesgue integrable on the open half-line \((0, \infty)\).

This generalizes the convergence of the integral \(\int_0^\infty x^{a-1} e^{-x} \, dx\) defining \(\Gamma(a)\), which is the case \(s = 1\).

theorem integrableOn_rpow_mul_exp_neg_mul_Ioi {a s : ℝ} (ha : 0 < a)
    (hs : 0 < s) :
    IntegrableOn (fun x : ℝ => x ^ (a - 1) * Real.exp (-(s * x))) (Ioi 0)

Used by 3

Used byFiniteness of all moments of the exponential law · Exponential moments of the gamma distribution · Integrability of \(x^k e^{-cx}\) under the Gamma law

TheoremExponential moments of the gamma distribution#✓fully proved

Let \(a > 0\) and \(r > 0\). For every real \(t < r\), the function \(x \mapsto e^{tx}\) is integrable with respect to the gamma distribution with shape \(a\) and rate \(r\).

theorem integrable_exp_mul_gammaMeasure {a r t : ℝ} (ha : 0 < a) (hr : 0 < r)
    (ht : t < r) :
    Integrable (fun x : ℝ => Real.exp (t * x)) (gammaMeasure a r)

Uses 1 · Used by 3

Proof usesIntegrability of the scaled gamma integrand

Used byExponential moments of the chi-square distribution · Half-line of exponential integrability for the gamma distribution · Moment generating function of the gamma distribution

TheoremMoment generating function of the gamma distribution#✓fully proved

Let \(a > 0\) and \(r > 0\), and let \(X\) have the gamma distribution with shape \(a\) and rate \(r\). For every real \(t < r\), the moment generating function of \(X\) at \(t\) is \(\mathbb{E}[e^{tX}] = \left(\frac{r}{r - t}\right)^a\).

theorem mgf_gammaMeasure_of_lt {a r t : ℝ} (ha : 0 < a) (hr : 0 < r)
    (ht : t < r) :
    mgf id (gammaMeasure a r) t = (r / (r - t)) ^ a

Uses 1 · Used by 5

Proof usesExponential moments of the gamma distribution

Used byMean no-recombination probability under the neutral coalescent · Gamma generation interval · Moment generating function of the chi-square distribution · Moment generating function of the gamma law with shape and rate one half · Fisher's method for combining p-values

TheoremHalf-line of exponential integrability for the gamma distribution#✓fully proved

Let \(a > 0\) and \(r > 0\), and let \(S\) be the set of real \(t\) such that \(x \mapsto e^{tx}\) is integrable with respect to the gamma distribution with shape \(a\) and rate \(r\). Then the half-line \((-\infty, r)\) is contained in \(S\).

theorem Iio_subset_integrableExpSet_gammaMeasure {a r : ℝ} (ha : 0 < a)
    (hr : 0 < r) :
    Iio r ⊆ integrableExpSet id (gammaMeasure a r)

Uses 1 · Used by 2

Proof usesExponential moments of the gamma distribution

Used byExponential moments of the gamma law are finite exactly below the rate · A neighbourhood of zero of exponential integrability for the gamma distribution

TheoremA neighbourhood of zero of exponential integrability for the gamma distribution#✓fully proved

Let \(a > 0\), \(r > 0\) and \(0 < \varepsilon < r\), and let \(S\) be the set of real \(t\) such that \(x \mapsto e^{tx}\) is integrable with respect to the gamma distribution with shape \(a\) and rate \(r\). Then the interval \((-\varepsilon, \varepsilon)\) is contained in the interior of \(S\).

This is the form of hypothesis used to identify a distribution from its moment generating function on such an interval.

theorem Ioo_subset_interior_integrableExpSet_gammaMeasure {a r ε : ℝ}
    (ha : 0 < a) (hr : 0 < r) (hε : 0 < ε) (hεr : ε < r) :
    Ioo (-ε) ε ⊆ interior (integrableExpSet id (gammaMeasure a r))

Uses 1 · Used by 1

Proof usesHalf-line of exponential integrability for the gamma distribution

Used byThe square of a standard normal variable is chi-square with one degree of freedom

LemmaGamma function at \(a + k\) via the rising factorial#✓fully proved

Γ(a + k) = a⁽ᵏ⁾ Γ(a) for a > 0.

lemma Gamma_add_nat_eq {a : ℝ} (ha : 0 < a) (k : ℕ) :
    Real.Gamma (a + k) = (ascPochhammer ℝ k).eval a * Real.Gamma a

Used by 2

Used byGamma integrals · Gamma–Poisson conjugacy, posterior

Lemma\(r^k r^{a-1} = r^{a+k-1}\) for nonnegative \(r\)#✓fully proved

rᵏ r^(a - 1) = r^(a + k - 1) for r ≥ 0 and a > 0.

lemma pow_mul_rpow_sub_one {r a : ℝ} (hr : 0 ≤ r) (ha : 0 < a) (k : ℕ) :
    r ^ k * r ^ (a - 1) = r ^ (a + k - 1)

Used by 3

Used byIntegrability of \(x^k e^{-cx}\) under the Gamma law · Gamma integrals · Gamma–Poisson conjugacy, posterior

TheoremGamma law is concentrated on the nonnegative reals#✓fully proved

The Gamma law is concentrated on [0, ∞).

theorem ae_nonneg_gammaMeasure (a b : ℝ) : ∀ᵐ x ∂gammaMeasure a b, 0 ≤ x

Used by 2

Used byMean · Second moment

TheoremIntegrability of \(x^k e^{-cx}\) under the Gamma law#✓fully proved

For a, b > 0 and c ≥ 0, x ↦ x ^ k e^{-c x} is integrable for Gamma(a, b).

theorem integrable_pow_mul_exp_neg_mul_gammaMeasure {a b c : ℝ} (ha : 0 < a) (hb : 0 < b)
    (hc : 0 ≤ c) (k : ℕ) :
    Integrable (fun x => x ^ k * Real.exp (-(c * x))) (gammaMeasure a b)

Uses 2 · Used by 2

Proof usesIntegrability of the scaled gamma integrand · \(r^k r^{a-1} = r^{a+k-1}\) for nonnegative \(r\)

Used byGamma law has finite first moment · Gamma law has finite second moment

TheoremGamma integrals#✓fully proved

For shape a > 0, rate b > 0 and c ≥ 0, ∫ x ^ k e^{-c x} dGamma(a, b) = a⁽ᵏ⁾ bᵃ / (b + c) ^ (a + k).

theorem integral_pow_mul_exp_neg_mul_gammaMeasure {a b c : ℝ} (ha : 0 < a) (hb : 0 < b)
    (hc : 0 ≤ c) (k : ℕ) :
    ∫ x, x ^ k * Real.exp (-(c * x)) ∂gammaMeasure a b =
      (ascPochhammer ℝ k).eval a * b ^ a / (b + c) ^ (a + k)

Uses 2 · Used by 3

Proof usesGamma function at \(a + k\) via the rising factorial · \(r^k r^{a-1} = r^{a+k-1}\) for nonnegative \(r\)

Used byGamma–Poisson conjugacy, posterior · Greenwood–Yule · Gamma–Poisson conjugacy, posterior predictive

TheoremGamma law has finite first moment#✓fully proved

x ↦ x is integrable for Gamma(a, b).

theorem integrable_id_gammaMeasure {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    Integrable id (gammaMeasure a b)

Uses 1 · Used by 1

Proof usesIntegrability of \(x^k e^{-cx}\) under the Gamma law

Used byMean

TheoremGamma law has finite second moment#✓fully proved

x ↦ x² is integrable for Gamma(a, b).

theorem integrable_sq_gammaMeasure {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    Integrable (fun x => x ^ 2) (gammaMeasure a b)

Uses 1 · Used by 1

Proof usesIntegrability of \(x^k e^{-cx}\) under the Gamma law

Used bySecond moment

TheoremExponential moments of the gamma law are finite exactly below the rate#✓fully proved

The exponential moment E[exp (t X)] of a gamma (a, r) law is finite exactly for t < r.

theorem integrableExpSet_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    integrableExpSet id (gammaMeasure a r) = Iio r

Uses 1 · Used by 2

Proof usesHalf-line of exponential integrability for the gamma distribution

Used byMoment generating function determines the gamma law · Sum of squares of independent standard normals is chi-square

TheoremMoment generating function determines the gamma law#✓fully proved

MGF uniqueness for gamma laws: a real probability law whose MGF equals the gamma (a, r) MGF as a function on all of ℝ (both vanish where the exponential moment is infinite) is that gamma law.

theorem eq_gammaMeasure_of_mgf_eq {a r : ℝ} (ha : 0 < a) (hr : 0 < r) {ν : Measure ℝ}
    [IsProbabilityMeasure ν] (h : mgf id ν = mgf id (gammaMeasure a r)) :
    ν = gammaMeasure a r

Uses 1 · Used by 2

Proof usesExponential moments of the gamma law are finite exactly below the rate

Used byFisher's method for combining p-values · Sum of squares of independent standard normals is chi-square

DefinitionUpper incomplete gamma function#✓fully proved

The upper incomplete gamma function Γ(a, x) = ∫_x^∞ t ^ (a - 1) e^{-t} dt (DLMF 8.2.2). The domain used below is a > 0 and x ≥ 0, where the integral converges. Outside it the Bochner integral may be the junk value 0 (for a ≤ 0, x = 0 the integrand is not integrable).

noncomputable def upperIncompleteGamma (a x : ℝ) : ℝ :=
  ∫ t in Ioi x, t ^ (a - 1) * exp (-t)

Used by 8

Used byFraction of mutations in a strength interval under the gamma DFE · Fraction of strongly deleterious mutations · Upper tail of the gamma law · Erlang tail formula · Recurrence for the upper incomplete gamma function · Upper incomplete gamma function at natural shapes · Upper incomplete gamma function with shape one · Upper incomplete gamma function at zero

TheoremUpper incomplete gamma function at zero#✓fully proved

Γ(a, 0) = Γ(a) for a > 0.

theorem upperIncompleteGamma_zero {a : ℝ} (ha : 0 < a) : upperIncompleteGamma a 0 = Gamma a

Uses 1 · Used by 1

Statement usesUpper incomplete gamma function

Used byRecurrence for the upper incomplete gamma function

TheoremUpper incomplete gamma function with shape one#✓fully proved

Γ(1, x) = e^{-x}.

theorem upperIncompleteGamma_one (x : ℝ) : upperIncompleteGamma 1 x = exp (-x)

Uses 1 · Used by 1

Statement usesUpper incomplete gamma function

Used byUpper incomplete gamma function at natural shapes

TheoremRecurrence for the upper incomplete gamma function#✓fully proved

The recurrence Γ(a + 1, x) = x ^ a e^{-x} + a Γ(a, x) for a > 0 and x ≥ 0 (DLMF 8.8.2), from integration by parts.

theorem upperIncompleteGamma_add_one {a x : ℝ} (ha : 0 < a) (hx : 0 ≤ x) :
    upperIncompleteGamma (a + 1) x = x ^ a * exp (-x) + a * upperIncompleteGamma a x

Uses 2 · Used by 1

Statement usesUpper incomplete gamma function

Proof usesUpper incomplete gamma function at zero

Used byUpper incomplete gamma function at natural shapes

TheoremUpper incomplete gamma function at natural shapes#✓fully proved

The closed form at natural shapes (DLMF 8.4.8): for x ≥ 0, Γ(n + 1, x) = n! e^{-x} ∑_{k = 0}^{n} x ^ k / (k!).

theorem upperIncompleteGamma_natCast_add_one (n : ℕ) {x : ℝ} (hx : 0 ≤ x) :
    upperIncompleteGamma (n + 1) x =
      Nat.factorial n * exp (-x) *
        ∑ k ∈ Finset.range (n + 1), x ^ k / Nat.factorial k

Uses 3 · Used by 1

Statement usesUpper incomplete gamma function

Proof usesRecurrence for the upper incomplete gamma function · Upper incomplete gamma function with shape one

Used byErlang tail formula

TheoremReal moments of the gamma law#✓fully proved

Real moments of the gamma law: for shape a > 0, rate r > 0 and p > -a, E[X ^ p] = Γ(a + p) / (Γ(a) r ^ p). (The law is carried by [0, ∞), so the values of x ^ p for x < 0 play no role.)

theorem integral_rpow_gammaMeasure {a r p : ℝ} (ha : 0 < a) (hr : 0 < r) (hp : -a < p) :
    ∫ x, x ^ p ∂gammaMeasure a r = Gamma (a + p) / (Gamma a * r ^ p)

Used by 3

Used byMean of the gamma law · Second moment of the gamma law · Gamma law has finite second moment

TheoremMean of the gamma law#✓fully proved

The mean of the gamma law with shape a > 0 and rate r > 0 is a / r.

theorem integral_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ x, x ∂gammaMeasure a r = a / r

Uses 1 · Used by 4

Proof usesReal moments of the gamma law

Used byMean selection coefficient under the gamma DFE · Variance of the gamma law · Mean · Second moment

TheoremSecond moment of the gamma law#✓fully proved

The second moment of the gamma law with shape a > 0 and rate r > 0 is a (a + 1) / r ^ 2.

theorem integral_sq_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ x, x ^ 2 ∂gammaMeasure a r = a * (a + 1) / r ^ 2

Uses 1 · Used by 2

Proof usesReal moments of the gamma law

Used byVariance of the gamma law · Second moment

TheoremGamma law has finite second moment#✓fully proved

The gamma law has finite second moment.

theorem memLp_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    MemLp id 2 (gammaMeasure a r)

Uses 1 · Used by 1

Proof usesReal moments of the gamma law

Used byVariance of the gamma law

TheoremVariance of the gamma law#✓fully proved

The variance of the gamma law with shape a > 0 and rate r > 0 is a / r ^ 2.

theorem variance_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    variance id (gammaMeasure a r) = a / r ^ 2

Uses 3 · Used by 1

Proof usesMean of the gamma law · Second moment of the gamma law · Gamma law has finite second moment

Used byVariance of the selection coefficient under the gamma DFE

TheoremScaling a gamma random variable#✓fully proved

Scaling a gamma variable by c > 0 keeps its shape and divides its rate by c: c X ~ Gamma(a, r / c) when X ~ Gamma(a, r).

theorem gammaMeasure_map_const_mul {a r c : ℝ} (ha : 0 < a) (hr : 0 < r) (hc : 0 < c) :
    (gammaMeasure a r).map (fun x => c * x) = gammaMeasure a (r / c)

Used by 1

Used byRescaling a gamma DFE divides its rate

TheoremUpper tail of the gamma law#✓fully proved

The upper tail of the gamma law: P(X > c) = Γ(a, r c) / Γ(a) for c ≥ 0.

theorem gammaMeasure_real_Ioi {a r c : ℝ} (ha : 0 < a) (hr : 0 < r) (hc : 0 ≤ c) :
    (gammaMeasure a r).real (Ioi c) = upperIncompleteGamma a (r * c) / Gamma a

Uses 1 · Used by 3

Statement usesUpper incomplete gamma function

Used byFraction of mutations in a strength interval under the gamma DFE · Fraction of strongly deleterious mutations · Erlang tail formula

TheoremErlang tail formula#✓fully proved

The Erlang tail: for shape n + 1, P(X > c) = e^{-r c} ∑_{k = 0}^{n} (r c) ^ k / (k!) when c ≥ 0.

theorem gammaMeasure_real_Ioi_natCast_add_one (n : ℕ) {r c : ℝ} (hr : 0 < r) (hc : 0 ≤ c) :
    (gammaMeasure (n + 1) r).real (Ioi c) =
      exp (-(r * c)) * ∑ k ∈ Finset.range (n + 1), (r * c) ^ k / Nat.factorial k

Uses 3 · Used by 1

Proof usesUpper tail of the gamma law · Upper incomplete gamma function · Upper incomplete gamma function at natural shapes

Used byPoisson–Gamma duality

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.