Quantiles of inverse-gamma laws

For positive shape a and scale r, the inverse-gamma quantile at an interior level u is r / inverseRegularizedGamma a (1 - u). Here r is the rate of the Gamma law whose reciprocal defines the inverse-gamma law. The quantile tends to 0 and +∞ at the two endpoints, respectively; these one-sided limits are stated in EReal.

The formula uses the existing inverse regularized Gamma function and the inverse-gamma cdf. It also supplies the scalar quantile formula for inverse-gamma marginals of matrix laws.

theorem TauCeti.Probability.quantile_inverseGammaMeasure {a r u : ℝ} (hr : 0 < r) : (inverseGammaMeasure a r).quantile u = r / inverseRegularizedGamma a (1 - u)

The quantile of an inverse-gamma law with positive scale is the scale divided by the inverse regularized Gamma function at the complementary level. Outside the valid range of the shape and of the level both sides take the junk value 0.

theorem TauCeti.Probability.tendsto_quantile_inverseGammaMeasure_nhdsGT_zero {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : Filter.Tendsto (fun (u : ℝ) => ↑((inverseGammaMeasure a r).quantile u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The inverse-gamma quantile tends to the lower support endpoint 0 as the level tends to 0 from above.

theorem TauCeti.Probability.tendsto_quantile_inverseGammaMeasure_nhdsLT_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : Filter.Tendsto (fun (u : ℝ) => ↑((inverseGammaMeasure a r).quantile u)) (nhdsWithin 1 (Set.Iio 1)) (nhds ⊤)

The inverse-gamma quantile tends to infinity as the level tends to 1 from below.