Moments, means, variances, and covariances of the real Dirichlet distribution

theorem ProbabilityTheory.integral_dirichletMeasure_power_product {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (m : ι → ℝ) (hm : b + m ∈ mvRealBetaDomain) : ∫ (u : ι → ℝ), ∏ i : ι, u i ^ m i ∂dirichletMeasure b = Real.Gamma (∑ i : ι, b i) / Real.Gamma (∑ i : ι, (b i + m i)) * ∏ i : ι, Real.Gamma (b i + m i) / Real.Gamma (b i)

The integral of a power product (generalized monomial) against the Dirichlet measure.

theorem ProbabilityTheory.integral_dirichletMeasure_monomial {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (m : ι → ℕ) : ∫ (u : ι → ℝ), ∏ i : ι, u i ^ m i ∂dirichletMeasure b = (∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℝ (m i))) / Polynomial.eval (∑ i : ι, b i) (ascPochhammer ℝ (∑ i : ι, m i))

The integral of a monomial against the Dirichlet measure.

theorem ProbabilityTheory.integral_dirichletMeasure_coordinate {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (i : ι) : ∫ (u : ι → ℝ), u i ∂dirichletMeasure b = b i / ∑ j : ι, b j

The mean of a single u i; a specialization of monomial integration.

theorem ProbabilityTheory.integral_dirichletMeasure_coordinate_sq {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (i : ι) : ∫ (u : ι → ℝ), u i ^ 2 ∂dirichletMeasure b = b i * (b i + 1) / ((∑ j : ι, b j) * (∑ j : ι, b j + 1))

The second raw moment of one coordinate under a Dirichlet measure.

theorem ProbabilityTheory.integral_dirichletMeasure_two_coordinates {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {i j : ι} (hij : i ≠ j) : ∫ (u : ι → ℝ), u i * u j ∂dirichletMeasure b = b i * b j / ((∑ k : ι, b k) * (∑ k : ι, b k + 1))

The mixed raw moment of two distinct coordinates under a Dirichlet measure.

theorem ProbabilityTheory.variance_dirichletMeasure_coordinate {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (i : ι) : ∫ (u : ι → ℝ), (u i - b i / ∑ j : ι, b j) ^ 2 ∂dirichletMeasure b = b i * (∑ j : ι, b j - b i) / ((∑ j : ι, b j) ^ 2 * (∑ j : ι, b j + 1))

The variance of the coordinate u i.

theorem ProbabilityTheory.covariance_dirichletMeasure_coordinate {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {i j : ι} (hij : i ≠ j) : ∫ (u : ι → ℝ), (u i - b i / ∑ k : ι, b k) * (u j - b j / ∑ k : ι, b k) ∂dirichletMeasure b = -b i * b j / ((∑ k : ι, b k) ^ 2 * (∑ k : ι, b k + 1))

The covariance of distinct coordinates u i and u j.