The inverse-gamma distribution: measure and density

The inverse-gamma law with shape a and scale r is the law of X⁻¹ for X ∼ gammaMeasure a r, where r is the Gamma rate. This file defines that pushforward for positive parameters and uses the zero measure otherwise. It derives the density

r ^ a / Gamma a * x ^ (-a - 1) * exp (-r / x)

on the positive half-line, proves its support and boundary behavior, identifies its Radon--Nikodym derivative, and proves parameter measurability.

The density is derived from the pushforward definition. On (0, ∞), inversion is an involution with absolute derivative x⁻²; the one-dimensional change of variables TauCeti.MeasureTheory.map_withDensity_abs_deriv_mul transports the Gamma density through this map.

Main declarations

• TauCeti.Probability.inverseGammaMeasure, inverseGammaPDFReal, and inverseGammaPDF define the law and its density;
• inverseGammaMeasure_eq_withDensity, hasPDF_of_hasLaw_inverseGammaMeasure, and rnDeriv_inverseGammaMeasure identify the density;
• inverseGammaMeasure_map_const_mul multiplies the scale under positive scaling;
• measurable_inverseGammaMeasure makes the parameterized family available to kernels.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley (1994), chapter on inverse-gamma distributions.

Definition and boundary behavior

noncomputable def TauCeti.Probability.inverseGammaMeasure (a r : ℝ) : MeasureTheory.Measure ℝ

The inverse-gamma law with shape a and scale r.

For positive parameters it is the pushforward of gammaMeasure a r by inversion, where r is the rate of the Gamma law. It is the zero measure if either parameter is nonpositive.

theorem TauCeti.Probability.inverseGammaMeasure_of_pos {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : inverseGammaMeasure a r = MeasureTheory.Measure.map Inv.inv (ProbabilityTheory.gammaMeasure a r)

At positive parameters the inverse-gamma law is the inversion pushforward of the Gamma law.

This is not a simp lemma: inverseGammaMeasure a r is the simp-normal form, and unfolding it would shadow every simp lemma stated about the law at positive parameters.

@[simp]

theorem TauCeti.Probability.inverseGammaMeasure_of_not_pos {a r : ℝ} (h : ¬(0 < a ∧ 0 < r)) : inverseGammaMeasure a r = 0

If the shape or scale is nonpositive, the inverse-gamma law is the zero measure.

theorem TauCeti.Probability.isProbabilityMeasure_inverseGammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (inverseGammaMeasure a r)

A valid inverse-gamma law is a probability measure.

@[simp]

theorem TauCeti.Probability.inverseGammaMeasure_Iic_zero (a r : ℝ) : (inverseGammaMeasure a r) (Set.Iic 0) = 0

The inverse-gamma law assigns no mass to the nonpositive half-line.

theorem TauCeti.Probability.ae_pos_inverseGammaMeasure (a r : ℝ) : ∀ᵐ (x : ℝ) ∂inverseGammaMeasure a r, 0 < x

An inverse-gamma law is concentrated on the positive half-line, including in the zero-measure invalid-parameter cases.

Density

noncomputable def TauCeti.Probability.inverseGammaPDFReal (a r x : ℝ) : ℝ

The real-valued inverse-gamma density. It vanishes unless both parameters and the sample point are positive.

noncomputable def TauCeti.Probability.inverseGammaPDF (a r x : ℝ) : ENNReal

The inverse-gamma density, valued in ℝ≥0∞.

theorem TauCeti.Probability.inverseGammaPDF_eq_ofReal (a r x : ℝ) : inverseGammaPDF a r x = ENNReal.ofReal (inverseGammaPDFReal a r x)

The ℝ≥0∞-valued inverse-gamma density is the coercion of the real-valued one.

@[simp]

theorem TauCeti.Probability.inverseGammaPDFReal_of_pos {a r x : ℝ} (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) : inverseGammaPDFReal a r x = r ^ a / Real.Gamma a * x ^ (-a - 1) * Real.exp (-r / x)

The real density has its usual formula at valid parameters and a positive point.

@[simp]

theorem TauCeti.Probability.inverseGammaPDFReal_of_nonpos {x : ℝ} (hx : x ≤ 0) (a r : ℝ) : inverseGammaPDFReal a r x = 0

The inverse-gamma density vanishes at a nonpositive point.

@[simp]

theorem TauCeti.Probability.inverseGammaPDFReal_of_not_pos {a r : ℝ} (h : ¬(0 < a ∧ 0 < r)) (x : ℝ) : inverseGammaPDFReal a r x = 0

The inverse-gamma density vanishes when its parameters are invalid.

@[simp]

theorem TauCeti.Probability.inverseGammaPDF_of_pos {a r x : ℝ} (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) : inverseGammaPDF a r x = ENNReal.ofReal (r ^ a / Real.Gamma a * x ^ (-a - 1) * Real.exp (-r / x))

The inverse-gamma density has its usual formula at valid parameters and a positive point.

@[simp]

theorem TauCeti.Probability.inverseGammaPDF_of_nonpos {x : ℝ} (hx : x ≤ 0) (a r : ℝ) : inverseGammaPDF a r x = 0

The inverse-gamma density vanishes at a nonpositive point.

@[simp]

theorem TauCeti.Probability.inverseGammaPDF_of_not_pos {a r : ℝ} (h : ¬(0 < a ∧ 0 < r)) (x : ℝ) : inverseGammaPDF a r x = 0

The inverse-gamma density vanishes when its parameters are invalid.

theorem TauCeti.Probability.inverseGammaPDFReal_nonneg (a r x : ℝ) : 0 ≤ inverseGammaPDFReal a r x

The real-valued inverse-gamma density is nonnegative.

@[simp]

theorem TauCeti.Probability.toReal_inverseGammaPDF (a r x : ℝ) : (inverseGammaPDF a r x).toReal = inverseGammaPDFReal a r x

Converting the inverse-gamma density back to ℝ recovers its real-valued version.

theorem TauCeti.Probability.measurable_inverseGammaPDFReal (a r : ℝ) : Measurable (inverseGammaPDFReal a r)

The real inverse-gamma density is measurable in the sample point.

theorem TauCeti.Probability.measurable_inverseGammaPDF (a r : ℝ) : Measurable (inverseGammaPDF a r)

The ℝ≥0∞-valued inverse-gamma density is measurable in the sample point.

theorem TauCeti.Probability.indicator_Ioi_inverseGammaPDF (a r : ℝ) : (Set.Ioi 0).indicator (inverseGammaPDF a r) = inverseGammaPDF a r

The inverse-gamma density is supported on the positive half-line.

theorem TauCeti.Probability.inverseGammaPDFReal_eq_inv_sq_mul_gammaPDFReal {a r x : ℝ} (ha : 0 < a) (hr : 0 < r) : inverseGammaPDFReal a r x = (x ^ 2)⁻¹ * ProbabilityTheory.gammaPDFReal a r x⁻¹

The inverse-gamma density is the Gamma density at the inverse point multiplied by the absolute Jacobian x⁻².

theorem TauCeti.Probability.inverseGammaMeasure_eq_withDensity (a r : ℝ) : inverseGammaMeasure a r = MeasureTheory.volume.withDensity (inverseGammaPDF a r)

The density of an inverse-gamma law, including the zero density at invalid parameters.

@[simp]

theorem TauCeti.Probability.inverseGammaMeasure_map_const_mul {b : ℝ} (hb : 0 < b) (a r : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => b * x) (inverseGammaMeasure a r) = inverseGammaMeasure a (b * r)

Scaling an inverse-gamma variable by b > 0 multiplies its scale by b. The identity also holds in the zero-measure invalid-parameter cases.

theorem TauCeti.Probability.hasPDF_of_hasLaw_inverseGammaMeasure {a r : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (inverseGammaMeasure a r) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random variable with an inverse-gamma law has a density.

theorem TauCeti.Probability.pdf_eq_inverseGammaPDF_of_hasLaw_inverseGammaMeasure {a r : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (inverseGammaMeasure a r) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] inverseGammaPDF a r

The density of a random variable with an inverse-gamma law is inverseGammaPDF.

theorem TauCeti.Probability.rnDeriv_inverseGammaMeasure (a r : ℝ) : (inverseGammaMeasure a r).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] inverseGammaPDF a r

The Radon–Nikodym derivative of an inverse-gamma law against Lebesgue measure.

Parameter measurability

theorem TauCeti.Probability.measurable_inverseGammaMeasure : Measurable fun (p : ℝ × ℝ) => inverseGammaMeasure p.1 p.2

The inverse-gamma family is jointly measurable in its parameters.