Analytic dependence of convergent Dirichlet integrals

This module proves parameter analyticity on the domain of absolute convergence. Continuation beyond that domain is developed separately in Dirichlet.Transform.

theorem ProbabilityTheory.analyticOnNhd_prod_invGamma {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (b : ι → ℂ) => ∏ i : ι, (Complex.Gamma (b i))⁻¹) Set.univ

The product of reciprocal Gamma factors used to regularize a Dirichlet integral is entire in the parameter vector.

theorem ProbabilityTheory.hasFDerivAt_mvBetaMonomial {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : ∀ (i : ι), 0 < u i) (b : ι → ℂ) : HasFDerivAt (fun (c : ι → ℂ) => ∏ i : ι, ↑(u i) ^ (c i - 1)) (∑ i : ι, (Complex.log ↑(u i) * ∏ j : ι, ↑(u j) ^ (b j - 1)) • ContinuousLinearMap.proj i) b

The Dirichlet monomial ∏ i, (u i) ^ (b i - 1) is entire in the parameter vector at every interior simplex point.

theorem ProbabilityTheory.regDirichletIntegral_analyticOn {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : AnalyticOn ℂ (fun (b : ι → ℂ) => regDirichletIntegral b f) Complex.mvBetaConvergent

If f is continuous on the closed standard simplex, then b ↦ regDirichletIntegral b f is analytic on the domain of absolute convergence.