Absolutely convergent complex Dirichlet monomial integrals

Real monomial integrability supplies the majorants for the complex beta integral and its logarithmic moments. This module imports neither the Dirichlet probability measure nor several-complex-variable analyticity or continuation.

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

The complex Dirichlet monomial is integrable on the simplex whenever every parameter has positive real part.

theorem Complex.integrableOn_mvBetaMonomial_mul_log {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (hb : b ∈ mvBetaConvergent) (i : ι) : MeasureTheory.IntegrableOn (fun (u : ι → ℝ) => (∏ j : ι, ↑(u j) ^ (b j - 1)) * log ↑(u i)) (Convexity.StdSimplex.coordinateSet ℝ ι) MeasureTheory.Measure.stdSimplexMeasure

Multiplying one factor of a convergent Dirichlet monomial by the logarithm of its coordinate preserves integrability. This is the basic domination estimate needed when differentiating a simplex Mellin integral with respect to a parameter.

theorem Complex.prod_cpow_stdSimplexCoordMap_scale {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) {t : ℝ} (ht : t ∈ Set.Ico 0 1) {v : { j : ι // j ≠ i } → ℝ} (hv : v ∈ Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }) : ∏ j : ι, ↑(stdSimplexCoordMap i (fun (q : { j : ι // j ≠ i }) => (1 - t) * v q) j) ^ (b j - 1) = (↑t ^ (b i - 1) * (1 - ↑t) ^ ∑ q : { j : ι // j ≠ i }, (b ↑q - 1)) * ∏ q : { j : ι // j ≠ i }, ↑(v q) ^ (b ↑q - 1)

A simplex slice separates a complex Dirichlet monomial into its distinguished-coordinate, radial, and lower-dimensional factors.

theorem Complex.mvBeta_eq_integral {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ mvBetaConvergent) : mvBeta b = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ∏ i : ι, ↑(u i) ^ (b i - 1) ∂MeasureTheory.Measure.stdSimplexMeasure

The absolutely convergent simplex integral representation of the multivariate Beta function.