The complex multivariate beta function

noncomputable def Complex.mvBeta {ι : Type u_1} [Fintype ι] (b : ι → ℂ) : ℂ

The multivariate Beta function.

Equations

• Complex.mvBeta b = (∏ i : ι, Complex.Gamma (b i)) / Complex.Gamma (∑ i : ι, b i)

def Complex.mvBetaConvergent {ι : Type u_1} : Set (ι → ℂ)

The domain on which the usual simplex integral representation of mvBeta converges absolutely.

Equations

• Complex.mvBetaConvergent = {b : ι → ℂ | ∀ (i : ι), 0 < (b i).re}

theorem Complex.isOpen_mvBetaConvergent {ι : Type u_1} [Finite ι] : IsOpen mvBetaConvergent

The ordinary Dirichlet convergence region is open.

theorem Complex.sum_re_pos_of_mem_mvBetaConvergent {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) : 0 < (∑ i : ι, b i).re

The sum of parameters in mvBetaConvergent has positive real part.

theorem Complex.mvBeta_ne_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) : mvBeta b ≠ 0

The multivariate Beta function does not vanish on its convergence domain.

theorem Complex.addNat_mem_mvBetaConvergent {ι : Type u_1} {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) (m : ι → ℕ) : (fun (i : ι) => b i + ↑(m i)) ∈ mvBetaConvergent

Adding nonnegative integers coordinatewise preserves mvBetaConvergent.

theorem Complex.comp_perm_mem_mvBetaConvergent {ι : Type u_1} {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) (σ : Equiv.Perm ι) : b ∘ ⇑σ ∈ mvBetaConvergent

Simultaneously permuting the parameters preserves the convergence domain.

theorem Complex.mvBeta_perm {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (σ : Equiv.Perm ι) : mvBeta (b ∘ ⇑σ) = mvBeta b

mvBeta is symmetric in its arguments.

theorem Complex.mvBeta_eq_one_of_unique {ι : Type u_1} [Fintype ι] [Unique ι] {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) : mvBeta b = 1

On a singleton index type, mvBeta equals one throughout its convergence domain.

theorem Complex.mvBeta_addNat_of_ne_neg_nat {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : ∀ (i : ι) (k : ℕ), b i ≠ -↑k) (m : ι → ℕ) : (mvBeta fun (i : ι) => b i + ↑(m i)) * Polynomial.eval (∑ i : ι, b i) (ascPochhammer ℂ (∑ i : ι, m i)) = mvBeta b * ∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))

Positive integer translates of mvBeta, assuming only that the coordinate parameters avoid the poles of the Gamma function. This hypothesis is substantially weaker than membership in mvBetaConvergent.

Some pole-avoidance hypothesis is necessary: because Mathlib totalizes Gamma to be zero at its poles, the displayed identity is not valid for arbitrary complex parameters.

theorem Complex.mvBeta_addNat {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) (m : ι → ℕ) : (mvBeta fun (i : ι) => b i + ↑(m i)) * Polynomial.eval (∑ i : ι, b i) (ascPochhammer ℂ (∑ i : ι, m i)) = mvBeta b * ∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))

Positive integer translates of mvBeta on its absolutely convergent domain.