Permutation, translation, and special values of S

theorem DirichletTransform.regCarlsonSIntegral_perm {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (σ : Equiv.Perm ι) : regCarlsonSIntegral (b ∘ ⇑σ) (z ∘ ⇑σ) = regCarlsonSIntegral b z

Simultaneous permutation of the Dirichlet parameters and variables leaves the native regularized S integral unchanged.

theorem DirichletTransform.regCarlsonSIntegral_add_const {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (a : ℂ) : (regCarlsonSIntegral b fun (i : ι) => z i + a) = Complex.exp a * regCarlsonSIntegral b z

Translating every variable by a multiplies the native regularized S integral by exp a. This is Carlson's exponential translation identity.

theorem DirichletTransform.regCarlsonSSeries_add_const {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) (a : ℂ) : regCarlsonSSeries (fun (i : ι) => z i + a) b = Complex.exp a * regCarlsonSSeries z b

Translation of all variables for Carlson's analytically continued S function. This global identity follows from the native integral identity and uniqueness of continuation in the Dirichlet parameters.

theorem DirichletTransform.regCarlsonSIntegral_zero {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : (regCarlsonSIntegral b fun (x : ι) => 0) = 1 / Complex.Gamma (∑ i : ι, b i)

At the zero variable vector, the native regularized S integral is the reciprocal Gamma factor on the ordinary convergence domain.