Carlson's homogeneity recurrence on the entire parameter space #
Relation 8.4-1 is a polynomial identity after Gamma regularization. Its coefficients therefore introduce no exceptional parameter values. This file extends the native integral proof by permanence of functional relations.
theorem
DirichletTransform.sum_carlsonAssociatedRecurrencePolynomial_mul_rContinued
{ι : Type u_1}
[Fintype ι]
[Nonempty ι]
(a : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRVariableDomain)
:
∑ n ∈ Finset.range (Fintype.card ι + 1),
(MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n a (∑ i : ι, b i - a) b) * regCarlsonRContinued (-a - ↑n) z hz b = 0
Carlson 8.4-1 for the continued regularized R-function, with arbitrary complex exponent and Dirichlet parameters, including zeros of the recurrence coefficients. Nodes remain in the existing right-half-plane domain.