The real multivariate beta function

noncomputable def ProbabilityTheory.mvRealBeta {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : ℝ

The multivariate real Beta function.

Equations

• ProbabilityTheory.mvRealBeta b = (∏ i : ι, Real.Gamma (b i)) / Real.Gamma (∑ i : ι, b i)

def ProbabilityTheory.mvRealBetaDomain {ι : Type u_1} : Set (ι → ℝ)

Domain for b where the Beta function is defined as an integral.

Equations

• ProbabilityTheory.mvRealBetaDomain = {b : ι → ℝ | ∀ (i : ι), 0 < b i}

theorem ProbabilityTheory.mvRealBeta_pos {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : 0 < mvRealBeta b

mvRealBeta is positive on mvRealBetaDomain.