Regularized complex Dirichlet integrals on the standard simplex

This file defines regularized complex Dirichlet densities and their associated integral functionals. These are complex-valued densities, not measures in the sense of Mathlib's nonnegative Measure type. Parameter analyticity is in Dirichlet.Complex.Analytic, and continuation beyond the convergence domain is in Dirichlet.Transform.

Main definitions and results

• Complex.mvBeta_eq_integral: the simplex integral representation of the multivariate Beta function.
• regDirichletDensity: the pointwise entire regularized Dirichlet density.
• complexDirichletDensity: the corresponding normalized complex density.
• regDirichletIntegral: integration against the regularized density.
• complexDirichletIntegral: integration against the normalized density.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Academic Press, 1977.

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

The regularized Dirichlet density with parameters b on stdSimplexInterior. For each fixed u, this is an entire function of b.

Equations

• ProbabilityTheory.regDirichletDensity b u = ProbabilityTheory.stdSimplexInterior.indicator (fun (u : ι → ℝ) => ∏ i : ι, ↑(u i) ^ (b i - 1) / Complex.Gamma (b i)) u

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

The normalized complex Dirichlet density with parameters b on stdSimplexInterior.

Equations

• ProbabilityTheory.complexDirichletDensity b u = Complex.Gamma (∑ i : ι, b i) * ProbabilityTheory.regDirichletDensity b u

theorem ProbabilityTheory.regDirichletDensity_perm {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (σ : Equiv.Perm ι) (u : ι → ℝ) : regDirichletDensity (b ∘ ⇑σ) (u ∘ ⇑σ) = regDirichletDensity b u

Simultaneously permuting the parameters and coordinates leaves the regularized Dirichlet density unchanged.

theorem ProbabilityTheory.measurable_regDirichletDensity {ι : Type u_1} [Fintype ι] (b : ι → ℂ) : Measurable (regDirichletDensity b)

The regularized Dirichlet density is a measurable function.

theorem ProbabilityTheory.regDirichletIntegral_normalization {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, regDirichletDensity b u ∂MeasureTheory.Measure.stdSimplexMeasure = 1 / Complex.Gamma (∑ i : ι, b i)

The regularized Dirichlet density integrated over the standard simplex.

theorem ProbabilityTheory.integrableOn_regDirichletDensity_mul {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : MeasureTheory.IntegrableOn (fun (u : ι → ℝ) => regDirichletDensity b u * f u) (Convexity.StdSimplex.coordinateSet ℝ ι) MeasureTheory.Measure.stdSimplexMeasure

Continuous functions are integrable over the standard simplex with respect to the regularized Dirichlet density.

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

Integration of function f over the standard simplex with respect to the regularized Dirichlet density. This is the native, totalized Bochner integral, not its analytic continuation outside the convergence domain.

Equations

• ProbabilityTheory.regDirichletIntegral b f = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ProbabilityTheory.regDirichletDensity b u * f u ∂MeasureTheory.Measure.stdSimplexMeasure

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

The normalized complex Dirichlet integral, defined using the native density. Outside the absolute-convergence domain this is a totalized Bochner integral, not an analytic continuation.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.complexDirichletIntegral_eq_gamma_mul {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (f : (ι → ℝ) → ℂ) : complexDirichletIntegral b f = Complex.Gamma (∑ i : ι, b i) * regDirichletIntegral b f

Native normalization and regularization differ by the Gamma factor of the total parameter. No assertion of analytic continuation is involved.

theorem ProbabilityTheory.regDirichletIntegral_eq_prod_invGamma_mul {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (f : (ι → ℝ) → ℂ) : regDirichletIntegral b f = (∏ i : ι, (Complex.Gamma (b i))⁻¹) * ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, (∏ i : ι, ↑(u i) ^ (b i - 1)) * f u ∂MeasureTheory.Measure.stdSimplexMeasure

Regularization amounts to multiplying the native, totalized simplex Mellin integral by the product of reciprocal Gamma factors. This identity does not require convergence.

theorem ProbabilityTheory.regDirichletIntegral_add {ι : Type u_1} [Fintype ι] (b : ι → ℂ) {f g : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) (hg : ContinuousOn g (Convexity.StdSimplex.coordinateSet ℝ ι)) (hb : b ∈ Complex.mvBetaConvergent) : (regDirichletIntegral b fun (u : ι → ℝ) => f u + g u) = regDirichletIntegral b f + regDirichletIntegral b g

regDirichletIntegral is additive.

theorem ProbabilityTheory.regDirichletIntegral_smul {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (f : (ι → ℝ) → ℂ) (c : ℂ) : (regDirichletIntegral b fun (u : ι → ℝ) => c * f u) = c * regDirichletIntegral b f

regDirichletIntegral commutes with complex scalar multiplication.

theorem ProbabilityTheory.regDirichletIntegral_congr {ι : Type u_1} [Fintype ι] (b : ι → ℂ) {f g : (ι → ℝ) → ℂ} (hfg : Set.EqOn f g (Convexity.StdSimplex.coordinateSet ℝ ι)) : regDirichletIntegral b f = regDirichletIntegral b g

The integral of f depends only on the values of f on the standard Simplex.