Beta distribution

TheoremNonnegativity of the beta density#✓fully proved

The beta density is nonnegative for positive shape parameters.

theorem betaPDFReal_nonneg {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (x : ℝ) :
    0 ≤ betaPDFReal α β x

Used by 4

Used byIntegrability of the mutation generator under Wright's stationary law · Weak stationarity of Wright's law (Wright 1931; Ewens 2004, ch. 4) · Integrals against the beta law · Beta density integrates to one

TheoremBeta density integrates to one#✓fully proved

The beta density integrates to 1 (the Bochner-integral form of lintegral_betaPDF_eq_one).

theorem integral_betaPDFReal {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∫ x, betaPDFReal α β x = 1

Uses 1 · Used by 1

Proof usesNonnegativity of the beta density

Used byMixed moments of the beta law

TheoremIntegrals against the beta law#✓fully proved

An integral against betaMeasure α β is the integral of the function times the beta density. No integrability hypothesis is needed: both sides are the junk value 0 together.

theorem integral_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (g : ℝ → ℝ) :
    ∫ x, g x ∂betaMeasure α β = ∫ x, betaPDFReal α β x * g x

Uses 1 · Used by 1

Proof usesNonnegativity of the beta density

Used byMixed moments of the beta law

TheoremRecurrence of the beta function in the first argument#✓fully proved

B(α + 1, β) = B(α, β) · α / (α + β).

theorem beta_add_one_left {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    beta (α + 1) β = beta α β * (α / (α + β))

Used by 3

Used byMean of the beta law · Mean of \(X(1 - X)\) under a beta law · Second moment of the beta law

TheoremSymmetry of the beta function#✓fully proved

The beta function is symmetric.

theorem beta_comm (α β : ℝ) : beta α β = beta β α

Used by 1

Used byMean of \(X(1 - X)\) under a beta law

TheoremBeta-function identity for densities#✓fully proved

Multiplying the Beta(α, β) density by x ^ k (1 - x) ^ m gives B(α + k, β + m) / B(α, β) times the Beta(α + k, β + m) density.

theorem betaPDFReal_mul_pow {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (k m : ℕ) (x : ℝ) :
    betaPDFReal α β x * (x ^ k * (1 - x) ^ m) =
      beta (α + k) (β + m) / beta α β * betaPDFReal (α + k) (β + m) x

Used by 1

Used byMixed moments of the beta law

TheoremMixed moments of the beta law#✓fully proved

For α, β > 0 and natural k, m, E[X ^ k (1 - X) ^ m] = B(α + k, β + m) / B(α, β).

theorem integral_pow_mul_one_sub_pow_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β)
    (k m : ℕ) :
    ∫ x, x ^ k * (1 - x) ^ m ∂betaMeasure α β = beta (α + k) (β + m) / beta α β

Uses 3 · Used by 3

Proof usesBeta-function identity for densities · Integrals against the beta law · Beta density integrates to one

Used byMean of the beta law · Mean of \(X(1 - X)\) under a beta law · Second moment of the beta law

TheoremMean of the beta law#✓fully proved

For α, β > 0, E[X] = α / (α + β).

theorem integral_id_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∫ x, x ∂betaMeasure α β = α / (α + β)

Uses 2 · Used by 2

Proof usesRecurrence of the beta function in the first argument · Mixed moments of the beta law

Used byMean proportion of a Dirichlet process · Second moment of \(1 - X\) under \(\mathrm{Beta}(1, \alpha)\)

TheoremSecond moment of the beta law#✓fully proved

For α, β > 0, E[X ^ 2] = α (α + 1) / ((α + β) (α + β + 1)).

theorem integral_sq_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∫ x, x ^ 2 ∂betaMeasure α β = α * (α + 1) / ((α + β) * (α + β + 1))

Uses 2 · Used by 2

Proof usesRecurrence of the beta function in the first argument · Mixed moments of the beta law

Used bySecond moment of \(1 - X\) under \(\mathrm{Beta}(1, \alpha)\) · Probability that two Dirichlet process draws pick the same piece

TheoremMean of \(X(1 - X)\) under a beta law#✓fully proved

For α, β > 0, E[X (1 - X)] = α β / ((α + β) (α + β + 1)) (half the expected heterozygosity of a Beta(α, β) allele frequency).

theorem integral_mul_one_sub_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∫ x, x * (1 - x) ∂betaMeasure α β = α * β / ((α + β) * (α + β + 1))

Uses 3

Proof usesRecurrence of the beta function in the first argument · Symmetry of the beta function · Mixed moments of the beta law

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.