← Copula mathematical handbook

Small-ball behaviour of the gamma law

For a gamma law with shape a > 0 and rate b > 0 and q ≥ 0,

K e^{-bq} q^a ≤ P(G < q) ≤ K q^a, K = b^a / (a Γ(a)),

so P(G < q) ~ K q^a as q → 0⁺ (regular variation of the gamma law at the origin). With q = m² / x² this gives x^{2a} P(G < m²/x²) → K m^{2a} as x → ∞, the form used for the tail of Student-t scale mixtures G^{-1/2} Z (where P(G^{-1/2} m ≥ x) = P(G ≤ m²/x²)).

Main results

• gammaMeasure_real_Iio_le, le_gammaMeasure_real_Iio: the two-sided small-ball bounds.
• rpow_mul_gammaMeasure_real_Iio_le, tendsto_rpow_mul_gammaMeasure_real_Iio: the scaled form.

References

• P. Embrechts, A. McNeil, D. Straumann, Correlation and dependence in risk management: properties and pitfalls, in: Risk Management: Value at Risk and Beyond, CUP 2002.

noncomputable def ProbabilityTheory.gammaSmallBallConst (a b : ℝ) : ℝ

The small-ball constant b^a / (a Γ(a)) of the gamma law with shape a and rate b.

Equations

• ProbabilityTheory.gammaSmallBallConst a b = b ^ a / (a * Real.Gamma a)

theorem ProbabilityTheory.gammaSmallBallConst_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < gammaSmallBallConst a b

theorem ProbabilityTheory.gammaMeasure_real_Iio_eq {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {q : ℝ} (hq : 0 ≤ q) : (gammaMeasure a b).real (Set.Iio q) = ∫ (x : ℝ) in 0..q, gammaPDFReal a b x

P(G < q) as an interval integral of the gamma density.

theorem ProbabilityTheory.gammaMeasure_real_Iio_le {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {q : ℝ} (hq : 0 ≤ q) : (gammaMeasure a b).real (Set.Iio q) ≤ gammaSmallBallConst a b * q ^ a

Upper small-ball bound: P(G < q) ≤ b^a q^a / (a Γ(a)).

theorem ProbabilityTheory.le_gammaMeasure_real_Iio {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {q : ℝ} (hq : 0 ≤ q) : gammaSmallBallConst a b * q ^ a * Real.exp (-(b * q)) ≤ (gammaMeasure a b).real (Set.Iio q)

Lower small-ball bound: b^a q^a e^{-bq} / (a Γ(a)) ≤ P(G < q).

theorem ProbabilityTheory.sq_rpow_eq_rpow_two_mul {m : ℝ} (hm : 0 ≤ m) (a : ℝ) : (m ^ 2) ^ a = m ^ (2 * a)

(m²)^a = m^{2a} for m ≥ 0.

theorem ProbabilityTheory.rpow_mul_div_sq_rpow {m x : ℝ} (hm : 0 ≤ m) (hx : 0 < x) (a : ℝ) : x ^ (2 * a) * (m ^ 2 / x ^ 2) ^ a = m ^ (2 * a)

x^{2a} (m²/x²)^a = m^{2a} for m ≥ 0 and x > 0.

theorem ProbabilityTheory.rpow_mul_gammaMeasure_real_Iio_le {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {m x : ℝ} (hm : 0 ≤ m) (hx : 0 < x) : x ^ (2 * a) * (gammaMeasure a b).real (Set.Iio (m ^ 2 / x ^ 2)) ≤ gammaSmallBallConst a b * m ^ (2 * a)

Scaled upper bound: x^{2a} P(G < m²/x²) ≤ K m^{2a}.

theorem ProbabilityTheory.le_rpow_mul_gammaMeasure_real_Iio {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {m x : ℝ} (hm : 0 ≤ m) (hx : 0 < x) : gammaSmallBallConst a b * m ^ (2 * a) * Real.exp (-(b * (m ^ 2 / x ^ 2))) ≤ x ^ (2 * a) * (gammaMeasure a b).real (Set.Iio (m ^ 2 / x ^ 2))

Scaled lower bound: K m^{2a} e^{-b m²/x²} ≤ x^{2a} P(G < m²/x²).

theorem ProbabilityTheory.tendsto_rpow_mul_gammaMeasure_real_Iio {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {m : ℝ} (hm : 0 ≤ m) : Filter.Tendsto (fun (x : ℝ) => x ^ (2 * a) * (gammaMeasure a b).real (Set.Iio (m ^ 2 / x ^ 2))) Filter.atTop (nhds (gammaSmallBallConst a b * m ^ (2 * a)))

Regular variation of the gamma law at the origin, scaled form: x^{2a} P(G < m²/x²) → b^a m^{2a} / (a Γ(a)) as x → ∞.