Documentation

TauCeti.Probability.Distributions.Gamma.Cdf

The cumulative distribution function of a gamma law #

This file computes ProbabilityTheory.cdf (gammaMeasure a r) in closed form: for a positive shape a and a positive rate r it is the regularized lower incomplete gamma function TauCeti.regularizedGamma read at the rate-scaled point, P(a, r * x).

This is the gamma entry of the closed-form cdf target of TauCetiRoadmap/StandardDistributions/README.md, Layer 2.

The identity holds for every real x, with no sign hypothesis: below the support both sides vanish, because TauCeti.regularizedGamma is extended by 0 there. That agreement at the clamping convention is the reason the roadmap prescribes the totalizations it does.

The computation is one change of variables. Mathlib's ProbabilityTheory.cdf_gammaMeasure_eq_integral presents the cdf as the integral of gammaPDFReal a r over Set.Iic x; the density vanishes below the origin, so for 0 < x that integral is the interval integral over 0..x. Collecting the rate into the variable, the integrand becomes Γ(a)⁻¹ * r * ((r * t) ^ (a - 1) * exp (-(r * t))), so intervalIntegral.integral_comp_mul_left at c = r turns it into Γ(a)⁻¹ * ∫ u in 0..r * x, u ^ (a - 1) * exp (-u), which is P(a, r * x) by definition.

At shape a = 1 the result recovers Mathlib's ProbabilityTheory.cdf_expMeasure_eq, since ProbabilityTheory.expMeasure r is gammaMeasure 1 r and TauCeti.regularizedGamma_one evaluates P(1, y) as 1 - exp (-y); this is the exponential completion check of the same layer.

Main results #

References #

Reduction of the cdf integral to the positive half-line #

The closed form #

source
@[simp]
theorem TauCeti.Probability.cdf_gammaMeasure_eq {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
↑(ProbabilityTheory.cdf (ProbabilityTheory.gammaMeasure a r)) x = regularizedGamma a (r * x)

The cumulative distribution function of the gamma law with shape a and rate r is the regularized lower incomplete gamma function evaluated at the rate-scaled point, P(a, r * x).

No sign hypothesis on x is needed: below the support both sides are 0, which is exactly the clamping convention built into TauCeti.regularizedGamma.

Consequences #

source
@[simp]
theorem TauCeti.Probability.measureReal_Iic_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
(ProbabilityTheory.gammaMeasure a r).real (Set.Iic x) = regularizedGamma a (r * x)

The mass a gamma law assigns to a lower half-line, in measure form.

source
@[simp]
theorem TauCeti.Probability.measureReal_Ioc_gammaMeasure {a r x : ℝ} (ha : 0 < a) (hr : 0 < r) {y : ℝ} (hyx : y ≤ x) :
(ProbabilityTheory.gammaMeasure a r).real (Set.Ioc y x) = regularizedGamma a (r * x) - regularizedGamma a (r * y)

The mass a gamma law assigns to a bounded interval is the increment of P(a, r * ·).

source
@[simp]
theorem TauCeti.Probability.measureReal_Ioi_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
(ProbabilityTheory.gammaMeasure a r).real (Set.Ioi x) = 1 - regularizedGamma a (r * x)

The upper tail of a gamma law is 1 - P(a, r * x).

source
theorem TauCeti.Probability.continuous_cdf_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.gammaMeasure a r))

The cumulative distribution function of a gamma law is continuous: P(a, ·) is continuous even at the origin, where for a < 1 Euler's integrand blows up.

source
theorem TauCeti.Probability.measureReal_le_of_hasLaw_gammaMeasure {a r : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (ha : 0 < a) (hr : 0 < r) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) (x : ℝ) :
P.real {ω : Ω | X ω ≤ x} = regularizedGamma a (r * x)

A random variable with a gamma law has the regularized lower incomplete gamma function as its cumulative distribution function.