Gamma distributions over ℝ

Define the gamma measure over the reals.

Main definitions

• gammaPDFReal: the function a r x ↦ r ^ a / (Gamma a) * x ^ (a - 1) * exp (-(r * x)) for 0 ≤ x or 0 else, which is the probability density function of a gamma distribution with shape a and rate r (when ha : 0 < a and hr : 0 < r).
• gammaPDF: ℝ≥0∞-valued pdf, gammaPDF a r = ENNReal.ofReal (gammaPDFReal a r).
• gammaMeasure: a gamma measure on ℝ, parametrized by its shape a and rate r.

theorem lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ENNReal) (hzy : z ≤ y) : ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x

A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x

noncomputable def ProbabilityTheory.gammaPDFReal (a r x : ℝ) : ℝ

The pdf of the gamma distribution depending on its scale and rate

noncomputable def ProbabilityTheory.gammaPDF (a r x : ℝ) : ENNReal

The pdf of the gamma distribution, as a function valued in ℝ≥0∞

theorem ProbabilityTheory.gammaPDF_eq (a r x : ℝ) : gammaPDF a r x = ENNReal.ofReal (if 0 ≤ x then r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)) else 0)

theorem ProbabilityTheory.gammaPDF_of_neg {a r x : ℝ} (hx : x < 0) : gammaPDF a r x = 0

theorem ProbabilityTheory.gammaPDF_of_nonneg {a r x : ℝ} (hx : 0 ≤ x) : gammaPDF a r x = ENNReal.ofReal (r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)))

theorem ProbabilityTheory.lintegral_gammaPDF_of_nonpos {x a r : ℝ} (hx : x ≤ 0) : ∫⁻ (y : ℝ) in Set.Iio x, gammaPDF a r y = 0

The Lebesgue integral of the gamma pdf over nonpositive reals equals 0

theorem ProbabilityTheory.measurable_gammaPDFReal (a r : ℝ) : Measurable (gammaPDFReal a r)

The gamma pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_gammaPDFReal (a r : ℝ) : MeasureTheory.StronglyMeasurable (gammaPDFReal a r)

The gamma pdf is strongly measurable

theorem ProbabilityTheory.gammaPDFReal_pos {x a r : ℝ} (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) : 0 < gammaPDFReal a r x

The gamma pdf is positive for all positive reals

theorem ProbabilityTheory.gammaPDFReal_nonneg {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : 0 ≤ gammaPDFReal a r x

The gamma pdf is nonnegative

@[simp]

theorem ProbabilityTheory.lintegral_gammaPDF_eq_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : ∫⁻ (x : ℝ), gammaPDF a r x = 1

The pdf of the gamma distribution integrates to 1

noncomputable def ProbabilityTheory.gammaMeasure (a r : ℝ) : MeasureTheory.Measure ℝ

Measure defined by the gamma distribution

theorem ProbabilityTheory.isProbabilityMeasure_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (gammaMeasure a r)

theorem ProbabilityTheory.cdf_gammaMeasure_eq_integral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : ↑(cdf (gammaMeasure a r)) x = ∫ (x : ℝ) in Set.Iic x, gammaPDFReal a r x

theorem ProbabilityTheory.cdf_gammaMeasure_eq_lintegral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : ↑(cdf (gammaMeasure a r)) x = (∫⁻ (x : ℝ) in Set.Iic x, gammaPDF a r x).toReal