Documentation

LeanPool.CarlsonFunctions.Carlson.R.ContinuedRecurrence

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.