Beta distributions over ℝ

Define the beta distribution over the reals.

Main definitions

• betaPDFReal: the function α β x ↦ (1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1) for 0 < x ∧ x < 1 or 0 else, which is the probability density function of a beta distribution with shape parameters α and β (when 0 < α and 0 < β).
• betaPDF: ℝ≥0∞-valued pdf, betaPDF α β = ENNReal.ofReal (betaPDFReal α β).

noncomputable def ProbabilityTheory.beta (α β : ℝ) : ℝ

The normalizing constant in the beta distribution.

theorem ProbabilityTheory.beta_pos {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : 0 < beta α β

theorem ProbabilityTheory.beta_eq_betaIntegralReal (α β : ℝ) (hα : 0 < α) (hβ : 0 < β) : beta α β = ((↑α).betaIntegral ↑β).re

Relation between the beta function and the gamma function over the reals.

noncomputable def ProbabilityTheory.betaPDFReal (α β x : ℝ) : ℝ

The probability density function of the beta distribution with shape parameters α and β. Returns (1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1) when 0 < x < 1 and 0 otherwise.

noncomputable def ProbabilityTheory.betaPDF (α β x : ℝ) : ENNReal

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

theorem ProbabilityTheory.betaPDF_eq (α β x : ℝ) : betaPDF α β x = ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0)

theorem ProbabilityTheory.betaPDF_eq_zero_of_nonpos {α β x : ℝ} (hx : x ≤ 0) : betaPDF α β x = 0

theorem ProbabilityTheory.betaPDF_eq_zero_of_one_le {α β x : ℝ} (hx : 1 ≤ x) : betaPDF α β x = 0

theorem ProbabilityTheory.betaPDF_of_pos_lt_one {α β x : ℝ} (hx_pos : 0 < x) (hx_lt : x < 1) : betaPDF α β x = ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

theorem ProbabilityTheory.lintegral_betaPDF {α β : ℝ} : ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

theorem ProbabilityTheory.betaPDFReal_pos {α β x : ℝ} (hx1 : 0 < x) (hx2 : x < 1) (hα : 0 < α) (hβ : 0 < β) : 0 < betaPDFReal α β x

The beta pdf is positive for all positive reals with positive parameters.

theorem ProbabilityTheory.measurable_betaPDFReal (α β : ℝ) : Measurable (betaPDFReal α β)

The beta pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_betaPDFReal (α β : ℝ) : MeasureTheory.StronglyMeasurable (betaPDFReal α β)

The beta pdf is strongly measurable.

@[simp]

theorem ProbabilityTheory.lintegral_betaPDF_eq_one {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : ∫⁻ (x : ℝ), betaPDF α β x = 1

The pdf of the beta distribution integrates to 1.

noncomputable def ProbabilityTheory.betaMeasure (α β : ℝ) : MeasureTheory.Measure ℝ

Measure defined by the beta distribution.

theorem ProbabilityTheory.isProbabilityMeasureBeta {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : MeasureTheory.IsProbabilityMeasure (betaMeasure α β)