Analytic dependence on the exponent of Carlson's R-integral

Unlike the Dirichlet parameters, the exponent has no convergence restriction on the right-half-plane node domain. This is the continuation input for fixed-parameter recurrences initially obtained from a convergent single-integral representation.

theorem DirichletTransform.hasDerivAt_regCarlsonRIntegral_exponent {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => regCarlsonRIntegral s b z) (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => carlsonAffineForm z u ^ t * Complex.log (carlsonAffineForm z u)) t

Differentiation in the exponent inserts the logarithm of the affine form into the regularized Dirichlet integral.

theorem DirichletTransform.analyticOnNhd_regCarlsonRIntegral_exponent {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (t : ℂ) => regCarlsonRIntegral t b z) Set.univ

The regularized native R-integral is entire in its exponent.

theorem DirichletTransform.analyticOnNhd_carlsonRIntegral_exponent {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (t : ℂ) => carlsonRIntegral t b z) Set.univ

The normalized native R-integral is entire in its exponent.