Euler transformations of Carlson's R-function

Carlson's Theorem 6.8-3 is proved on the full product slit plane and for arbitrary complex exponents and Dirichlet parameters, in the entire regularized normalization. The proof first reflects the beta integral on right-half-plane nodes, then uses permanence of functional relations in the parameters and in the nodes. Theorem 6.8-4's additional equal-parameter regularization remains a separate task.

theorem DirichletTransform.carlsonRVariableDomain_inv {ι : Type u_1} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : (fun (i : ι) => (z i)⁻¹) ∈ carlsonRVariableDomain

Taking reciprocals preserves the right-half-plane node domain.

theorem DirichletTransform.carlsonRUnitIntervalIntegral_inv {ι : Type u_1} [Fintype ι] (a a' : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : carlsonRUnitIntervalIntegral a a' b z = (∏ i : ι, z i ^ (-b i)) * carlsonRUnitIntervalIntegral a' a b fun (i : ι) => (z i)⁻¹

Reflection of the beta integral, with principal branches controlled by positivity of the real parts of each factor.

theorem DirichletTransform.regCarlsonRContinued_euler {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued t z hz b = (∏ i : ι, z i ^ (-b i)) * regCarlsonRContinued (-∑ i : ι, b i - t) (fun (i : ι) => (z i)⁻¹) ⋯ b

Euler's transformation (Carlson 6.8-3), entire in the exponent and every Dirichlet parameter. No Gamma-regularity or convergence assumptions are needed.

theorem DirichletTransform.regCarlsonRSlit_euler {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : regCarlsonRSlit t b z = (∏ i : ι, z i ^ (-b i)) * regCarlsonRSlit (-∑ i : ι, b i - t) b fun (i : ι) => (z i)⁻¹

Euler inversion (Carlson's Theorem 6.8-3) on the full product slit plane, for all complex exponents and Dirichlet parameters.