Elementary theory of the gamma distribution

This file develops the elementary moment theory of Mathlib's gamma distribution. For a positive shape a and a positive rate r it computes every natural raw moment, the mean and the variance, every natural inverse moment that exists, the exact set of rates at which an exponential moment exists, and the moment- and cumulant-generating functions on that set. It also identifies the law of a positive rescaling: only the rate moves, and it moves by the scaling factor. Finally, it proves that the convolution of two gamma laws with the same rate adds their shape parameters.

The moment and transform computations go through the same two reductions. The measure gammaMeasure a r is volume.withDensity of a density carried by [0, ∞), so an integral against it is a set integral of the weighted integrand over (0, ∞), and integrability against it is integrability of that same weighted integrand over (0, ∞). Raw moments and exponential moments then both reduce to Euler's integral through Real.integral_rpow_mul_exp_neg_mul_Ioi, whose shape x ^ (s - 1) * exp (-(b * x)) they match after collecting exponents: a factor x ^ n shifts the shape from a to a + n, and a factor exp (t * x) shifts the rate from r to r - t. The second shift explains the exponential moment domain: it is exactly the half-line on which the shifted rate is still positive. A factor (x ^ n)⁻¹ shifts the shape the other way, from a to a - n, and Euler's integral converges exactly when that shifted shape is still positive, which is the inverse-moment threshold n < a.

Main results

• TauCeti.Probability.integrable_gammaMeasure_iff and TauCeti.Probability.integral_gammaMeasure_eq — integrability and integration against the gamma law, transferred to the real density;
• TauCeti.Probability.integral_pow_gammaMeasure — the natural raw moments, Γ (a + n) / (Γ a * r ^ n), with TauCeti.Probability.integral_id_gammaMeasure and TauCeti.Probability.integral_sq_gammaMeasure as the first two cases;
• TauCeti.Probability.integrable_inv_pow_gammaMeasure_iff — the nth inverse power is integrable exactly below the shape, n < a, and TauCeti.Probability.integral_inv_pow_gammaMeasure — that inverse moment is r ^ n * Γ (a - n) / Γ a;
• TauCeti.Probability.variance_id_gammaMeasure — the variance is a / r ^ 2;
• TauCeti.Probability.integrable_exp_mul_id_gammaMeasure and TauCeti.Probability.not_integrable_exp_mul_id_gammaMeasure — the exponential moment of rate t exists exactly when t < r, recorded as an equality of sets in TauCeti.Probability.integrableExpSet_id_gammaMeasure;
• TauCeti.Probability.mgf_id_gammaMeasure — the moment-generating function is (1 - t / r) ^ (-a) there;
• TauCeti.Probability.cgf_id_gammaMeasure — the cumulant-generating function is -a * log (1 - t / r) there, the real logarithm of the previous formula;
• TauCeti.Probability.gammaMeasure_conv_gammaMeasure — convolution at a common rate adds the shape parameters;
• TauCeti.Probability.gammaMeasure_map_const_mul — scaling by c > 0 sends the rate r to r / c;
• TauCeti.Probability.gammaMeasure_eq_withDensity_restrict_Ioi — the law is its density against Lebesgue measure on Ioi 0;

The cumulative distribution function is computed in TauCeti/Probability/Distributions/Gamma/Cdf.lean.

References

• Tau Ceti roadmap, StandardDistributions, Layer 1, "Gamma".
• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley, 1994, ch. 17.

instance TauCeti.Probability.instSigmaFiniteRealGammaMeasure_tauCeti (a r : ℝ) : MeasureTheory.SigmaFinite (ProbabilityTheory.gammaMeasure a r)

A Gamma measure is sigma-finite for all parameter values.

Reduction to the positive half-line

theorem TauCeti.Probability.ae_pos_gammaMeasure (a r : ℝ) : ∀ᵐ (x : ℝ) ∂ProbabilityTheory.gammaMeasure a r, 0 < x

A gamma measure is almost everywhere strictly positive, for all parameter values.

theorem TauCeti.Probability.gammaMeasure_eq_withDensity_restrict_Ioi (a r : ℝ) : ProbabilityTheory.gammaMeasure a r = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity (ProbabilityTheory.gammaPDF a r)

The gamma law is its density against Lebesgue measure on the open positive half-line: the density vanishes below the origin, and the origin itself is null.

theorem TauCeti.Probability.ae_mem_prod_Ioi_gammaMeasure {a r b s : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hs : 0 < s) : ∀ᵐ (z : ℝ × ℝ) ∂(ProbabilityTheory.gammaMeasure a r).prod (ProbabilityTheory.gammaMeasure b s), z ∈ Set.Ioi 0 ×ˢ Set.Ioi 0

Almost every point of a product of two gamma laws with positive parameters lies in the open positive quadrant.

@[simp]

theorem TauCeti.Probability.gammaPDFReal_of_nonneg {a r x : ℝ} (hx : 0 ≤ x) : ProbabilityTheory.gammaPDFReal a r x = r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x))

Off the negative half-line the gamma density is given by its closed formula.

theorem TauCeti.Probability.gammaMeasure_eq_withDensity_ofReal (a r : ℝ) : ProbabilityTheory.gammaMeasure a r = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.gammaPDFReal a r x)

The gamma law presented by its real-valued density.

theorem TauCeti.Probability.integrable_gammaMeasure_iff {a r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ha : 0 < a) (hr : 0 < r) {g : ℝ → E} : MeasureTheory.Integrable g (ProbabilityTheory.gammaMeasure a r) ↔ MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.gammaPDFReal a r x • g x) MeasureTheory.volume

Integrability transfer. A function is integrable against a gamma law with positive shape and rate exactly when its density-weighted version is Lebesgue integrable.

theorem TauCeti.Probability.integral_gammaMeasure_eq {a r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ha : 0 < a) (hr : 0 < r) (g : ℝ → E) : ∫ (x : ℝ), g x ∂ProbabilityTheory.gammaMeasure a r = ∫ (x : ℝ), ProbabilityTheory.gammaPDFReal a r x • g x

Integral transfer. An integral against a gamma law with positive shape and rate is the density-weighted Lebesgue integral.

theorem TauCeti.Probability.integral_gammaMeasure_eq_integral_Ioi {a r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ha : 0 < a) (hr : 0 < r) (f : ℝ → E) : ∫ (x : ℝ), f x ∂ProbabilityTheory.gammaMeasure a r = ∫ (x : ℝ) in Set.Ioi 0, (r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x))) • f x

An integral against the gamma law is the set integral of the weighted integrand over (0, ∞).

Raw moments, mean and variance

@[simp]

theorem TauCeti.Probability.integral_pow_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (n : ℕ) : ∫ (x : ℝ), x ^ n ∂ProbabilityTheory.gammaMeasure a r = Real.Gamma (a + ↑n) / (Real.Gamma a * r ^ n)

The nth raw moment of a gamma law with positive shape and rate.

@[simp]

theorem TauCeti.Probability.integrable_inv_pow_gammaMeasure_iff {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => (x ^ n)⁻¹) (ProbabilityTheory.gammaMeasure a r) ↔ ↑n < a

The nth inverse power is integrable under a Gamma law exactly when n is below the shape.

@[simp]

theorem TauCeti.Probability.integral_inv_pow_gammaMeasure {a r : ℝ} (hr : 0 < r) (n : ℕ) (hn : ↑n < a) : ∫ (x : ℝ), (x ^ n)⁻¹ ∂ProbabilityTheory.gammaMeasure a r = r ^ n * Real.Gamma (a - ↑n) / Real.Gamma a

The nth inverse moment of a Gamma law, when n is below the shape.

@[simp]

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

The mean of a gamma law with positive shape and rate is a / r.

@[simp]

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

The second raw moment of a gamma law with positive shape and rate is a * (a + 1) / r ^ 2.

Exponential moments

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

Below the rate of a gamma law, its exponential moments exist.

theorem TauCeti.Probability.integrable_pow_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (ProbabilityTheory.gammaMeasure a r)

Every natural power is integrable under a gamma law with positive shape and rate.

theorem TauCeti.Probability.memLp_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.MemLp id 2 (ProbabilityTheory.gammaMeasure a r)

The identity function belongs to L² of a gamma law with positive shape and rate.

theorem TauCeti.Probability.not_integrable_exp_mul_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) {t : ℝ} (ht : r ≤ t) : ¬MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (ProbabilityTheory.gammaMeasure a r)

At or above the rate of a gamma law, its exponential moments do not exist.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : ProbabilityTheory.integrableExpSet id (ProbabilityTheory.gammaMeasure a r) = Set.Iio r

The exponential moments of a gamma law of rate r are exactly those of rate t < r.

@[simp]

theorem TauCeti.Probability.mgf_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) {t : ℝ} (ht : t < r) : ProbabilityTheory.mgf id (ProbabilityTheory.gammaMeasure a r) t = (1 - t / r) ^ (-a)

The moment-generating function of a gamma law on the half-line where its exponential moment is integrable, namely t < r.

@[simp]

theorem TauCeti.Probability.cgf_id_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) {t : ℝ} (ht : t < r) : ProbabilityTheory.cgf id (ProbabilityTheory.gammaMeasure a r) t = -a * Real.log (1 - t / r)

The cumulant-generating function of a gamma law on the half-line where its exponential moment is integrable, namely t < r. It is the real logarithm of TauCeti.Probability.mgf_id_gammaMeasure.

@[simp]

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

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

Convolution

@[simp]

theorem TauCeti.Probability.gammaMeasure_conv_gammaMeasure {a r b : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) : (ProbabilityTheory.gammaMeasure a r).conv (ProbabilityTheory.gammaMeasure b r) = ProbabilityTheory.gammaMeasure (a + b) r

The convolution of two gamma laws with a common positive rate is a gamma law whose shape is the sum of the two positive shapes.

Scaling

@[simp]

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

Scaling a gamma variable by c > 0 divides its rate by c.