The inverse regularized gamma function

Since the regularized lower incomplete gamma function P(s, ·) is the cumulative distribution function of the Gamma law with shape s and rate 1, its inverse is that law's quantile function. This file defines TauCeti.inverseRegularizedGamma through MeasureTheory.Measure.quantile and specializes the general quantile API to it.

For 0 < s and 0 < u < 1, TauCeti.inverseRegularizedGamma s u is the unique positive x such that P(s, x) = u. It is extended by 0 outside that parameter range.

Main definition

• TauCeti.inverseRegularizedGamma — the inverse P⁻¹(s, u) in the argument, defined through the quantile of ProbabilityTheory.gammaMeasure s 1.

Main results

• TauCeti.inverseRegularizedGamma_eq_quantile identifies the inverse with the Gamma quantile;
• TauCeti.inverseRegularizedGamma_le_iff is the Galois characterization P⁻¹(s, u) ≤ x ↔ u ≤ P(s, x);
• TauCeti.regularizedGamma_inverseRegularizedGamma and TauCeti.inverseRegularizedGamma_regularizedGamma are the two inverse identities;
• TauCeti.inverseRegularizedGamma_eq_iff gives uniqueness of the positive root;
• TauCeti.strictMonoOn_inverseRegularizedGamma, TauCeti.continuousOn_inverseRegularizedGamma, TauCeti.tendsto_inverseRegularizedGamma_nhdsGT_zero, TauCeti.tendsto_inverseRegularizedGamma_nhdsLT_one, and TauCeti.measurable_inverseRegularizedGamma give regularity, endpoint limits, and joint measurability;
• TauCeti.inverseRegularizedGamma_one evaluates the inverse at shape 1.
• TauCeti.Probability.quantile_gammaMeasure gives the quantile of a Gamma law of arbitrary positive rate by scaling TauCeti.inverseRegularizedGamma;
• TauCeti.Probability.tendsto_quantile_gammaMeasure_nhdsGT_zero and TauCeti.Probability.tendsto_quantile_gammaMeasure_nhdsLT_one give its endpoint limits.

References

• NIST Digital Library of Mathematical Functions, §8.2.

noncomputable def TauCeti.inverseRegularizedGamma (s u : ℝ) : ℝ

The inverse P⁻¹(s, u) of the regularized lower incomplete gamma function in its argument.

For positive s this is the quantile of the Gamma law with shape s and rate 1. For nonpositive s it is 0; the quantile itself supplies the value 0 outside 0 < u < 1.

theorem TauCeti.inverseRegularizedGamma_eq_quantile {s u : ℝ} (hs : 0 < s) : inverseRegularizedGamma s u = (ProbabilityTheory.gammaMeasure s 1).quantile u

For positive shape, P⁻¹(s, ·) is the quantile function of the Gamma law with shape s and rate 1.

theorem TauCeti.inverseRegularizedGamma_eq_sInf {s u : ℝ} (hs : 0 < s) : inverseRegularizedGamma s u = sInf {x : ℝ | u ≤ regularizedGamma s x}

For positive shape, P⁻¹(s, u) is the infimum of the points at which P(s, ·) reaches u.

@[simp]

theorem TauCeti.inverseRegularizedGamma_eq_zero_of_nonpos_left {s : ℝ} (hs : s ≤ 0) (u : ℝ) : inverseRegularizedGamma s u = 0

Outside the valid range of the shape parameter, P⁻¹(s, u) is 0.

@[simp]

theorem TauCeti.inverseRegularizedGamma_eq_zero_of_nonpos_right {u : ℝ} (s : ℝ) (hu : u ≤ 0) : inverseRegularizedGamma s u = 0

At levels u ≤ 0, P⁻¹(s, u) is 0.

@[simp]

theorem TauCeti.inverseRegularizedGamma_eq_zero_of_one_le {u : ℝ} (s : ℝ) (hu : 1 ≤ u) : inverseRegularizedGamma s u = 0

At levels 1 ≤ u, P⁻¹(s, u) is 0.

theorem TauCeti.inverseRegularizedGamma_eq_zero_of_not {s u : ℝ} (h : ¬(0 < s ∧ u ∈ Set.Ioo 0 1)) : inverseRegularizedGamma s u = 0

P⁻¹(s, u) is 0 whenever s or u lies outside the valid range 0 < s, 0 < u < 1.

theorem TauCeti.setOf_le_regularizedGamma_eq_Ici {s u : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : {x : ℝ | u ≤ regularizedGamma s x} = Set.Ici (inverseRegularizedGamma s u)

The points at which P(s, ·) reaches a level u ∈ (0, 1) form the closed ray starting at P⁻¹(s, u).

theorem TauCeti.inverseRegularizedGamma_le_iff {s u x : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : inverseRegularizedGamma s u ≤ x ↔ u ≤ regularizedGamma s x

The Galois characterization of P⁻¹(s, ·): for a level u ∈ (0, 1), P⁻¹(s, u) ≤ x exactly when u ≤ P(s, x).

theorem TauCeti.lt_inverseRegularizedGamma_iff {s u x : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : x < inverseRegularizedGamma s u ↔ regularizedGamma s x < u

The negation of TauCeti.inverseRegularizedGamma_le_iff.

theorem TauCeti.inverseRegularizedGamma_pos {s u : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : 0 < inverseRegularizedGamma s u

P⁻¹(s, u) is positive, for 0 < s and 0 < u < 1.

theorem TauCeti.inverseRegularizedGamma_nonneg (s u : ℝ) : 0 ≤ inverseRegularizedGamma s u

P⁻¹(s, u) is nonnegative, for every parameter value.

@[simp]

theorem TauCeti.regularizedGamma_inverseRegularizedGamma {s u : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : regularizedGamma s (inverseRegularizedGamma s u) = u

P⁻¹(s, ·) is a right inverse of P(s, ·) on the levels 0 < u < 1.

theorem TauCeti.inverseRegularizedGamma_lt_iff {s u x : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : inverseRegularizedGamma s u < x ↔ u < regularizedGamma s x

The strict form of TauCeti.inverseRegularizedGamma_le_iff.

theorem TauCeti.inverseRegularizedGamma_eq_iff {s u x : ℝ} (hs : 0 < s) (hu : u ∈ Set.Ioo 0 1) : inverseRegularizedGamma s u = x ↔ regularizedGamma s x = u

Uniqueness: for 0 < s and 0 < u < 1, the only solution of P(s, x) = u is x = P⁻¹(s, u).

@[simp]

theorem TauCeti.inverseRegularizedGamma_regularizedGamma {s x : ℝ} (hs : 0 < s) (hx : 0 < x) : inverseRegularizedGamma s (regularizedGamma s x) = x

P⁻¹(s, ·) is a left inverse of P(s, ·) on the open half-line 0 < x.

theorem TauCeti.strictMonoOn_inverseRegularizedGamma {s : ℝ} (hs : 0 < s) : StrictMonoOn (inverseRegularizedGamma s) (Set.Ioo 0 1)

P⁻¹(s, ·) is strictly increasing on the levels 0 < u < 1.

theorem TauCeti.continuousOn_inverseRegularizedGamma {s : ℝ} (hs : 0 < s) : ContinuousOn (inverseRegularizedGamma s) (Set.Ioo 0 1)

P⁻¹(s, ·) is continuous on the levels 0 < u < 1.

theorem TauCeti.tendsto_inverseRegularizedGamma_nhdsGT_zero {s : ℝ} (hs : 0 < s) : Filter.Tendsto (inverseRegularizedGamma s) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))

P⁻¹(s, u) tends to 0 from above as the level u decreases to 0.

theorem TauCeti.tendsto_inverseRegularizedGamma_nhdsLT_one {s : ℝ} (hs : 0 < s) : Filter.Tendsto (inverseRegularizedGamma s) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

P⁻¹(s, u) tends to ∞ as the level u increases to 1.

theorem TauCeti.measurable_inverseRegularizedGamma : Measurable fun (p : ℝ × ℝ) => inverseRegularizedGamma p.1 p.2

P⁻¹(s, u) is jointly measurable in the shape parameter and the level, including outside the valid parameter range.

theorem TauCeti.inverseRegularizedGamma_one {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : inverseRegularizedGamma 1 u = -Real.log (1 - u)

At shape 1, P⁻¹(1, u) = -log (1 - u): the inverse of the standard exponential cdf.

theorem TauCeti.Probability.quantile_gammaMeasure {u a r : ℝ} (ha : 0 < a) (hr : 0 < r) : (ProbabilityTheory.gammaMeasure a r).quantile u = inverseRegularizedGamma a u / r

The quantile of a Gamma law with positive shape a and rate r is P⁻¹(a, u) / r, where P⁻¹ is the inverse regularized lower incomplete Gamma function. Both sides are 0 outside the levels 0 < u < 1.

theorem TauCeti.Probability.tendsto_quantile_gammaMeasure_nhdsGT_zero {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : Filter.Tendsto (fun (u : ℝ) => (ProbabilityTheory.gammaMeasure a r).quantile u) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))

The quantile of a positive-parameter Gamma law tends to the lower support endpoint 0 as the level tends to 0 from above.

theorem TauCeti.Probability.tendsto_quantile_gammaMeasure_nhdsLT_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : Filter.Tendsto (fun (u : ℝ) => (ProbabilityTheory.gammaMeasure a r).quantile u) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

The quantile of a positive-parameter Gamma law tends to infinity as the level tends to 1 from below.