Dirichlet distribution

TheoremThe Beta integral#✓fully proved

For real numbers \(a > 0\) and \(b > 0\), the integral over the open interval \((0, 1)\), taken as a Lebesgue integral with values in \([0, \infty]\), is

\[\int_0^1 t^{a-1} (1 - t)^{b-1} \, dt = B(a, b),\]

where \(B(a, b) = \Gamma(a) \Gamma(b) / \Gamma(a + b)\) is the Beta function.

theorem lintegral_Ioo_rpow_mul_rpow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    ∫⁻ t in Ioo (0 : ℝ) 1, ENNReal.ofReal (t ^ (a - 1) * (1 - t) ^ (b - 1)) =
      ENNReal.ofReal (beta a b)

Used by 1

Used byThe Dirichlet integral

DefinitionUnnormalized Dirichlet density#✓fully proved

For parameters \(\alpha = (\alpha_0, \dots, \alpha_n) \in \mathbb{R}^{n+1}\), the unnormalized Dirichlet density is the function \(D_\alpha \colon \mathbb{R}^n \to [0, \infty]\) defined by

\[D_\alpha(x) = \Bigl(\prod_{i=0}^{n-1} x_i^{\alpha_i - 1}\Bigr) \Bigl(1 - \sum_{i=0}^{n-1} x_i\Bigr)^{\alpha_n - 1}\]

when \(x\) lies in the open corner simplex, that is \(x_i > 0\) for every \(i\) and \(\sum_{i=0}^{n-1} x_i < 1\), and by \(D_\alpha(x) = 0\) otherwise.

Here \(x\) stands for the first \(n\) coordinates of the probability vector \((x_0, \dots, x_{n-1}, 1 - \sum_{i=0}^{n-1} x_i)\).

noncomputable def dirichletDensity {n : ℕ} (α : Fin (n + 1) → ℝ) (x : Fin n → ℝ) : ℝ≥0∞ :=
  if (∀ i, 0 < x i) ∧ ∑ i, x i < 1 then
    ENNReal.ofReal ((∏ i, x i ^ (α (Fin.castSucc i) - 1)) * (1 - ∑ i, x i) ^ (α (Fin.last n) - 1))
  else 0

Used by 10

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · The Dirichlet distribution is concentrated on the open simplex · Splitting off the first coordinate of the Dirichlet density · Multiplying the Dirichlet density by a multinomial likelihood · Dirichlet distribution · The Dirichlet integral · The Dirichlet integral for a single parameter · Mean of the Dirichlet distribution · Dirichlet–multinomial conjugacy

DefinitionMultivariate Beta function#✓fully proved

For real parameters \(\alpha = (\alpha_0, \dots, \alpha_{n-1})\), the multivariate Beta function is

\[B(\alpha) = \frac{\prod_{i=0}^{n-1} \Gamma(\alpha_i)}{\Gamma(\sum_{i=0}^{n-1} \alpha_i)}.\]

It is the normalizing constant of the Dirichlet distribution.

noncomputable def multiBeta {n : ℕ} (α : Fin n → ℝ) : ℝ :=
  (∏ i, Gamma (α i)) / Gamma (∑ i, α i)

Used by 9

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · Evidence-weighted Dirichlet prior · The Dirichlet distribution is concentrated on the open simplex · Dirichlet distribution · The Dirichlet integral · The Dirichlet integral for a single parameter · Mean of the Dirichlet distribution · Dirichlet–multinomial conjugacy

TheoremThe Dirichlet integral for a single parameter#✓fully proved

Let \(\alpha = (\alpha_0) \in \mathbb{R}^1\) with \(\alpha_0 > 0\), let \(D_\alpha\) be the unnormalized Dirichlet density with parameters \(\alpha\), a function on \(\mathbb{R}^0\), and let \(B(\alpha)\) be the multivariate Beta function. Then \(\int_{\mathbb{R}^0} D_\alpha(x) \, dx = B(\alpha)\), the integral being taken with respect to Lebesgue measure.

Both sides equal \(1\): \(\mathbb{R}^0\) is a single point of measure \(1\), \(D_\alpha\) equals \(1\) there, and \(B(\alpha) = \Gamma(\alpha_0) / \Gamma(\alpha_0)\).

theorem lintegral_dirichletDensity_zero {α : Fin 1 → ℝ} (hα : ∀ i, 0 < α i) :
    ∫⁻ x, dirichletDensity α x = ENNReal.ofReal (multiBeta α)

Uses 2 · Used by 1

Statement usesUnnormalized Dirichlet density · Multivariate Beta function

Used byThe Dirichlet integral

TheoremTonelli's theorem for the first coordinate#✓fully proved

Let \(G \colon \mathbb{R}^{n+1} \to [0, \infty]\) be measurable. Then

\[\int_{\mathbb{R}^{n+1}} G(x) \, dx = \int_{\mathbb{R}} \int_{\mathbb{R}^n} G(t, y) \, dy \, dt\]

where \((t, y) \in \mathbb{R}^{n+1}\) denotes the vector with first coordinate \(t\) followed by the coordinates of \(y\), and all integrals are taken with respect to Lebesgue measure.

theorem lintegral_fin_succ {n : ℕ} {G : (Fin (n + 1) → ℝ) → ℝ≥0∞} (hG : Measurable G) :
    ∫⁻ x, G x = ∫⁻ t, ∫⁻ y, G (Fin.cons t y)

Used by 1

Used byThe Dirichlet integral

TheoremScaling the variable of a Lebesgue integral#✓fully proved

Let \(F \colon \mathbb{R}^n \to [0, \infty]\) be measurable and let \(c > 0\) be a real number. Then

\[\int_{\mathbb{R}^n} F(y) \, dy = c^n \int_{\mathbb{R}^n} F(c u) \, du\]

where both integrals are taken with respect to Lebesgue measure.

theorem lintegral_comp_smul_fin {n : ℕ} {F : (Fin n → ℝ) → ℝ≥0∞} (hF : Measurable F) {c : ℝ}
    (hc : 0 < c) : ∫⁻ y, F y = ENNReal.ofReal (c ^ n) * ∫⁻ u, F (c • u)

Used by 1

Used byThe Dirichlet integral

TheoremSplitting off the first coordinate of the Dirichlet density#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_{n+1}) \in \mathbb{R}^{n+2}\), write \(D_\alpha\) for the unnormalized Dirichlet density with parameters \(\alpha\) (a function on \(\mathbb{R}^{n+1}\)), and let \(\alpha' = (\alpha_1, \dots, \alpha_{n+1}) \in \mathbb{R}^{n+1}\). For every real \(t\) with \(0 < t < 1\) and every \(u \in \mathbb{R}^n\),

\[D_\alpha(t, (1 - t) u) = t^{\alpha_0 - 1} (1 - t)^{\alpha_1 + \dots + \alpha_{n+1} - 1 - n} D_{\alpha'}(u)\]

where \((t, (1 - t) u) \in \mathbb{R}^{n+1}\) is the vector with first coordinate \(t\) followed by the coordinates of \((1 - t) u\).

theorem dirichletDensity_cons_smul {n : ℕ} (α : Fin (n + 2) → ℝ) {t : ℝ} (ht0 : 0 < t)
    (ht1 : t < 1) (u : Fin n → ℝ) :
    dirichletDensity α (Fin.cons t ((1 - t) • u)) =
      ENNReal.ofReal (t ^ (α 0 - 1) * (1 - t) ^ (∑ j, α (Fin.succ j) - 1 - n)) *
        dirichletDensity (fun j ↦ α (Fin.succ j)) u

Uses 1 · Used by 1

Statement usesUnnormalized Dirichlet density

Used byThe Dirichlet integral

TheoremThe Dirichlet integral#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_n) \in \mathbb{R}^{n+1}\) with \(\alpha_i > 0\) for every \(i\), and let \(\Delta = \{x \in \mathbb{R}^n : x_i > 0 \text{ for all } i \text{ and } \sum_{i=0}^{n-1} x_i < 1\}\) be the open corner simplex. Then

\[\int_{\Delta} \Bigl(\prod_{i=0}^{n-1} x_i^{\alpha_i - 1}\Bigr) \Bigl(1 - \sum_{i=0}^{n-1} x_i\Bigr)^{\alpha_n - 1} dx = \frac{\prod_{i=0}^{n} \Gamma(\alpha_i)}{\Gamma\bigl(\sum_{i=0}^{n} \alpha_i\bigr)},\]

where \(dx\) is Lebesgue measure. Equivalently, the integral of the unnormalized Dirichlet density \(D_\alpha\) over \(\mathbb{R}^n\) equals the multivariate Beta function \(B(\alpha)\).

theorem lintegral_dirichletDensity {n : ℕ} {α : Fin (n + 1) → ℝ} (hα : ∀ i, 0 < α i) :
    ∫⁻ x, dirichletDensity α x = ENNReal.ofReal (multiBeta α)

Uses 7 · Used by 3

Statement usesUnnormalized Dirichlet density · Multivariate Beta function

Proof usesSplitting off the first coordinate of the Dirichlet density · The Beta integral · Scaling the variable of a Lebesgue integral · The Dirichlet integral for a single parameter · Tonelli's theorem for the first coordinate

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · Mean of the Dirichlet distribution

DefinitionSimplex completion#✓fully proved

For \(x = (x_0, \dots, x_{n-1}) \in \mathbb{R}^n\), the simplex completion of \(x\) is the vector \((x_0, \dots, x_{n-1}, 1 - \sum_{i=0}^{n-1} x_i) \in \mathbb{R}^{n+1}\), whose coordinates sum to \(1\).

def simplexCompletion {n : ℕ} (x : Fin n → ℝ) : Fin (n + 1) → ℝ :=
  Fin.snoc x (1 - ∑ i, x i)

Used by 7

Used byDirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · The Dirichlet distribution is concentrated on the open simplex · Multiplying the Dirichlet density by a multinomial likelihood · Dirichlet distribution · Mean of the Dirichlet distribution · Dirichlet–multinomial conjugacy

DefinitionDirichlet distribution#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_n) \in \mathbb{R}^{n+1}\), let \(D_\alpha\) be the unnormalized Dirichlet density on \(\mathbb{R}^n\) with parameters \(\alpha\), and let \(B(\alpha) = \prod_{i=0}^{n} \Gamma(\alpha_i) / \Gamma(\sum_{i=0}^{n} \alpha_i)\) be the multivariate Beta function. The Dirichlet distribution \(\mathrm{Dir}(\alpha)\) is the measure on \(\mathbb{R}^{n+1}\) obtained by pushing forward the measure on \(\mathbb{R}^n\) with density \(D_\alpha(x) / B(\alpha)\) with respect to Lebesgue measure along the map \(x \mapsto (x_0, \dots, x_{n-1}, 1 - \sum_{i=0}^{n-1} x_i)\).

The quotient is taken in \([0, \infty]\), with a nonpositive \(B(\alpha)\) read as \(0\); this matters only when some \(\alpha_i \le 0\). For positive parameters \(\mathrm{Dir}(\alpha)\) is a probability measure concentrated on vectors with positive entries summing to \(1\).

noncomputable def dirichletMeasure {n : ℕ} (α : Fin (n + 1) → ℝ) : Measure (Fin (n + 1) → ℝ) :=
  ((volume : Measure (Fin n → ℝ)).withDensity fun x ↦
    dirichletDensity α x / ENNReal.ofReal (multiBeta α)).map simplexCompletion

Uses 3 · Used by 8

Statement usesUnnormalized Dirichlet density · Multivariate Beta function · Simplex completion

Used byPrior predictive of the Dirichlet–categorical model · Dirichlet–multinomial conjugacy · Posterior predictive of the Dirichlet–multinomial model · Evidence-weighted Dirichlet prior · Finite-dimensional marginals of the Dirichlet process · The Dirichlet distribution is concentrated on the open simplex · Mean of the Dirichlet distribution · Dirichlet–multinomial conjugacy

TheoremThe Dirichlet distribution is concentrated on the open simplex#✓fully proved

For every \(n\) and every parameter vector \(\alpha \in \mathbb{R}^{n+1}\), almost every \(\theta \in \mathbb{R}^{n+1}\) with respect to the Dirichlet distribution \(\mathrm{Dir}(\alpha)\) is a probability vector with positive entries: \(\theta_i > 0\) for every \(i\) and \(\sum_{i=0}^{n} \theta_i = 1\).

theorem ae_dirichletMeasure {n : ℕ} (α : Fin (n + 1) → ℝ) :
    ∀ᵐ θ ∂dirichletMeasure α, (∀ i, 0 < θ i) ∧ ∑ i, θ i = 1

Uses 4 · Used by 2

Statement usesDirichlet distribution

Proof usesUnnormalized Dirichlet density · Multivariate Beta function · Simplex completion

Used byPrior predictive of the Dirichlet–categorical model · Evidence-weighted Dirichlet prior

TheoremMultiplying the Dirichlet density by a multinomial likelihood#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_n) \in \mathbb{R}^{n+1}\) and let \(k = (k_0, \dots, k_n)\) be natural numbers; write \(D_\beta\) for the unnormalized Dirichlet density with parameters \(\beta\). For every \(x \in \mathbb{R}^n\), let \(\theta = (x_0, \dots, x_{n-1}, 1 - \sum_{i=0}^{n-1} x_i)\) be its completion to a vector summing to \(1\), and write \(\theta_i^+ = \max(\theta_i, 0)\). Then

\[D_\alpha(x) \prod_{i=0}^{n} (\theta_i^+)^{k_i} = D_{\alpha + k}(x).\]

Both sides vanish unless \(x\) lies in the open corner simplex, where every \(\theta_i\) is positive and \(\theta_i^+ = \theta_i\).

theorem dirichletDensity_mul_prod_pow {n : ℕ} (α : Fin (n + 1) → ℝ) (k : Fin (n + 1) → ℕ)
    (x : Fin n → ℝ) :
    dirichletDensity α x * ∏ i, ENNReal.ofReal (simplexCompletion x i) ^ k i =
      dirichletDensity (fun i ↦ α i + k i) x

Uses 2 · Used by 1

Statement usesUnnormalized Dirichlet density · Simplex completion

Used byDirichlet–multinomial conjugacy

TheoremDirichlet–multinomial conjugacy#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_n)\) have positive real entries and let \(k = (k_0, \dots, k_n)\) be natural numbers (counts). The measure with density \(\theta \mapsto \prod_{i=0}^{n} \max(\theta_i, 0)^{k_i}\) with respect to the Dirichlet distribution \(\mathrm{Dir}(\alpha)\), that is, \(\mathrm{Dir}(\alpha)\) weighted by the likelihood of the counts \(k\), equals

\[\frac{B(\alpha + k)}{B(\alpha)} \, \mathrm{Dir}(\alpha + k),\]

where \(B\) is the multivariate Beta function and \(\alpha + k\) is taken entrywise.

theorem withDensity_prod_pow_dirichletMeasure {n : ℕ} {α : Fin (n + 1) → ℝ} (hα : ∀ i, 0 < α i)
    (k : Fin (n + 1) → ℕ) :
    (dirichletMeasure α).withDensity (fun θ ↦ ∏ i, ENNReal.ofReal (θ i) ^ k i) =
      ENNReal.ofReal (multiBeta (fun i ↦ α i + k i) / multiBeta α) •
        dirichletMeasure (fun i ↦ α i + k i)

Uses 5 · Used by 2

Statement usesDirichlet distribution · Multivariate Beta function

Proof usesUnnormalized Dirichlet density · Multiplying the Dirichlet density by a multinomial likelihood · Simplex completion

Used byEvidence-weighted Dirichlet prior · Mean of the Dirichlet distribution

TheoremMean of the Dirichlet distribution#✓fully proved

Let \(\alpha = (\alpha_0, \dots, \alpha_n) \in \mathbb{R}^{n+1}\) with \(\alpha_j > 0\) for every \(j\). For every \(i\), the \(i\)-th coordinate of a random vector \(\theta\) with the Dirichlet distribution \(\mathrm{Dir}(\alpha)\) has mean

\[\mathbb{E}[\theta_i] = \frac{\alpha_i}{\sum_{j=0}^{n} \alpha_j}.\]

Formally the left side is the integral of \(\max(\theta_i, 0)\) with respect to \(\mathrm{Dir}(\alpha)\); this is the mean of \(\theta_i\) because \(\theta_i > 0\) almost surely.

theorem lintegral_dirichletMeasure_apply {n : ℕ} {α : Fin (n + 1) → ℝ} (hα : ∀ i, 0 < α i)
    (i : Fin (n + 1)) :
    ∫⁻ θ, ENNReal.ofReal (θ i) ∂dirichletMeasure α = ENNReal.ofReal (α i / ∑ j, α j)

Uses 6 · Used by 1

Statement usesDirichlet distribution

Proof usesUnnormalized Dirichlet density · The Dirichlet integral · Multivariate Beta function · Simplex completion · Dirichlet–multinomial conjugacy

Used byPrior predictive of the Dirichlet–categorical model

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.