Bridge between real and complex Carlson averages

This file identifies the probability average at positive real parameters with the regularized complex Carlson integral.

theorem DirichletTransform.regCarlsonDirichletAverage_ofReal {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ ProbabilityTheory.mvRealBetaDomain) (z : ι → ℂ) (f : ℂ → ℂ) : regCarlsonDirichletAverage (fun (i : ι) => ↑(b i)) z f = realCarlsonDirichletAverage b z f / Complex.Gamma (∑ i : ι, ↑(b i))

On positive real parameters, the regularized complex Carlson integral is the Dirichlet probability average divided by the Gamma factor of the total parameter.