Solid-simplex integral evaluation of multivariate beta

def Complex.mvBetaSimplex (n : ℕ) : Set (Fin n → ℝ)

The solid standard n-simplex used in the DLMF multivariate Beta integrals.

Equations

• Complex.mvBetaSimplex n = {x : Fin n → ℝ | (∀ (i : Fin n), 0 ≤ x i) ∧ ∑ i : Fin n, x i ≤ 1}

theorem Complex.measurableSet_mvBetaSimplex (n : ℕ) : MeasurableSet (mvBetaSimplex n)

The solid standard simplex is a measurable set.

noncomputable def Complex.mvBetaIntegral {n : ℕ} (b₀ : ℂ) (b : Fin n → ℂ) : ℂ

The solid-coordinate multivariate Beta integral. The parameter b₀ belongs to the slack coordinate 1 - ∑ i, x i, while b i belongs to x i. This is the integral on the left-hand side of DLMF 5.14.2.

Equations

• b₀.mvBetaIntegral b = ∫ (x : Fin n → ℝ) in Complex.mvBetaSimplex n, ↑(1 - ∑ i : Fin n, x i) ^ (b₀ - 1) * ∏ i : Fin n, ↑(x i) ^ (b i - 1)

noncomputable def Complex.mvBetaIntegralOne {n : ℕ} (b : Fin n → ℂ) : ℂ

The solid-coordinate integral in DLMF 5.14.1, in which the slack coordinate has exponent zero.

Equations

• Complex.mvBetaIntegralOne b = ∫ (x : Fin n → ℝ) in Complex.mvBetaSimplex n, ∏ i : Fin n, ↑(x i) ^ (b i - 1)

theorem Complex.mvBetaIntegral_eq_mvBeta {n : ℕ} {b₀ : ℂ} {b : Fin n → ℂ} (hb₀ : 0 < b₀.re) (hb : ∀ (i : Fin n), 0 < (b i).re) : b₀.mvBetaIntegral b = mvBeta (Fin.cons b₀ b)

DLMF 5.14.2: the solid-coordinate Dirichlet integral equals the multivariate Beta function. The slack parameter is placed first in Fin.cons; parameter symmetry identifies this convention with the DLMF convention, where it is displayed last.

theorem Complex.mvBetaIntegralOne_eq_mvBeta {n : ℕ} {b : Fin n → ℂ} (hb : ∀ (i : Fin n), 0 < (b i).re) : mvBetaIntegralOne b = mvBeta (Fin.cons 1 b)

DLMF 5.14.1: the solid-simplex integral without a slack-coordinate factor equals the multivariate Beta function with slack parameter one.