Moments of the inverse-gamma distribution

This file proves the real and natural moments, mean, variance, sharp moment thresholds, and exact exponential-integrability domain of the inverse-gamma distribution.

Moments

@[simp]

theorem TauCeti.Probability.integrable_rpow_inverseGammaMeasure_iff {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (q : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ q) (inverseGammaMeasure a r) ↔ q < a

A real power is integrable under a valid inverse-gamma law exactly when its exponent is below the shape parameter.

@[simp]

theorem TauCeti.Probability.integral_rpow_inverseGammaMeasure {a r q : ℝ} (ha : 0 < a) (hr : 0 < r) (hq : q < a) : ∫ (x : ℝ), x ^ q ∂inverseGammaMeasure a r = r ^ q * Real.Gamma (a - q) / Real.Gamma a

Real-power moments of a valid inverse-gamma law. The qth moment exists for q < a and equals r ^ q * Gamma (a - q) / Gamma a.

@[simp]

theorem TauCeti.Probability.integrable_pow_inverseGammaMeasure_iff {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (inverseGammaMeasure a r) ↔ ↑n < a

A natural power is integrable under a valid inverse-gamma law exactly below the shape.

@[simp]

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

Natural moments of a valid inverse-gamma law. The nth moment exists for n < a and equals r ^ n * Gamma (a - n) / Gamma a.

@[simp]

theorem TauCeti.Probability.integral_id_inverseGammaMeasure {a r : ℝ} (hr : 0 < r) (ha : 1 < a) : ∫ (x : ℝ), x ∂inverseGammaMeasure a r = r / (a - 1)

The mean of an inverse-gamma law is r / (a - 1) when 1 < a.

@[simp]

theorem TauCeti.Probability.integral_sq_inverseGammaMeasure {a r : ℝ} (hr : 0 < r) (ha : 2 < a) : ∫ (x : ℝ), x ^ 2 ∂inverseGammaMeasure a r = r ^ 2 / ((a - 1) * (a - 2))

The second raw moment of an inverse-gamma law is r² / ((a - 1) * (a - 2)) when 2 < a.

@[simp]

theorem TauCeti.Probability.variance_id_inverseGammaMeasure {a r : ℝ} (hr : 0 < r) (ha : 2 < a) : ProbabilityTheory.variance id (inverseGammaMeasure a r) = r ^ 2 / ((a - 1) ^ 2 * (a - 2))

The variance of an inverse-gamma law is r² / ((a - 1)² * (a - 2)) when 2 < a.

@[simp]

theorem TauCeti.Probability.integrable_id_inverseGammaMeasure_iff {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.Integrable id (inverseGammaMeasure a r) ↔ 1 < a

The identity is integrable under a valid inverse-gamma law exactly above shape one.

theorem TauCeti.Probability.not_integrable_id_inverseGammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (h : a ≤ 1) : ¬MeasureTheory.Integrable id (inverseGammaMeasure a r)

At and below shape one, the identity is not integrable under a valid inverse-gamma law.

theorem TauCeti.Probability.not_integrable_sq_inverseGammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (h : a ≤ 2) : ¬MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (inverseGammaMeasure a r)

At and below shape two, the square is not integrable under a valid inverse-gamma law.

Exponential moments

theorem TauCeti.Probability.integrable_exp_mul_inverseGammaMeasure {a r t : ℝ} (ht : t ≤ 0) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (inverseGammaMeasure a r)

Every nonpositive exponential moment of an inverse-gamma law exists. Invalid parameters give the zero measure.

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

Positive exponential moments of a valid inverse-gamma law do not exist.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_inverseGammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : ProbabilityTheory.integrableExpSet id (inverseGammaMeasure a r) = Set.Iic 0

The exact exponential-integrability domain of a valid inverse-gamma law is the nonpositive half-line.