Compatibility of real and complex Dirichlet integrals

At positive real parameters the normalized complex integral is a probability expectation; the regularized integral differs by the Gamma factor of the total parameter. These identities hold for arbitrary integrands as identities of totalized Bochner integrals. They neither require nor invoke analytic continuation.

@[simp]

theorem Complex.mvBeta_ofReal {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : (mvBeta fun (i : ι) => ↑(b i)) = ↑(ProbabilityTheory.mvRealBeta b)

The complex multivariate beta function specializes to the real one.

theorem DirichletTransform.regDirichletDensity_ofReal_eq {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ ProbabilityTheory.mvRealBetaDomain) (u : ι → ℝ) : ProbabilityTheory.regDirichletDensity (fun (i : ι) => ↑(b i)) u = ↑(ProbabilityTheory.dirichletPdfReal b u) / Complex.Gamma (∑ i : ι, ↑(b i))

For positive real parameters, the regularized complex density is the real Dirichlet probability density divided by the Gamma factor of the total parameter.

theorem ProbabilityTheory.complexDirichletDensity_ofReal {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (u : ι → ℝ) : complexDirichletDensity (fun (i : ι) => ↑(b i)) u = ↑(dirichletPdfReal b u)

At positive real parameters the normalized complex density is the real probability density, regarded as complex-valued.

theorem ProbabilityTheory.complexDirichletIntegral_ofReal {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (f : (ι → ℝ) → ℂ) : complexDirichletIntegral (fun (i : ι) => ↑(b i)) f = ∫ (u : ι → ℝ), f u ∂dirichletMeasure b

The normalized native complex Dirichlet integral is a probability expectation at positive real parameters.

theorem ProbabilityTheory.regDirichletIntegral_ofReal {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (f : (ι → ℝ) → ℂ) : regDirichletIntegral (fun (i : ι) => ↑(b i)) f = (∫ (u : ι → ℝ), f u ∂dirichletMeasure b) / Complex.Gamma (∑ i : ι, ↑(b i))

The regularized native complex Dirichlet integral is the probability expectation divided by the Gamma factor of the total parameter.

theorem ProbabilityTheory.complexDirichletIntegral_ofReal_ofReal {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (f : (ι → ℝ) → ℝ) : (complexDirichletIntegral (fun (i : ι) => ↑(b i)) fun (u : ι → ℝ) => ↑(f u)) = ∫ (u : ι → ℝ), ↑(f u) ∂dirichletMeasure b

Real-valued probability expectations can be recovered by specializing the complex Dirichlet integral in both its parameters and its integrand.