Real Dirichlet monomial integrals

Shared analytic foundations for the real probability distribution and complex Dirichlet integrals. No Dirichlet probability measure is constructed or imported here. The historical ProbabilityTheory declaration names are retained for compatibility.

theorem ProbabilityTheory.lintegral_dirichletMonomial_eq_mvRealBeta {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : ∫⁻ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ENNReal.ofReal (∏ i : ι, u i ^ (b i - 1)) ∂MeasureTheory.Measure.stdSimplexMeasure = ENNReal.ofReal (mvRealBeta b)

The nonnegative Dirichlet monomial integral, used to establish integrability before passing to the Bochner integral.

theorem ProbabilityTheory.mvRealBeta_eq_integral {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : mvRealBeta b = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ∏ i : ι, u i ^ (b i - 1) ∂MeasureTheory.Measure.stdSimplexMeasure

The integral representation of mvRealBeta.

theorem ProbabilityTheory.integrableOn_mvRealBetaMonomial {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : MeasureTheory.IntegrableOn (fun (u : ι → ℝ) => ∏ i : ι, u i ^ (b i - 1)) (Convexity.StdSimplex.coordinateSet ℝ ι) MeasureTheory.Measure.stdSimplexMeasure

A real Dirichlet monomial is integrable at positive parameters, including when the index type is empty. This is the shared majorant for complex Dirichlet integrals.