Associated L-relations with polynomial correction coefficients

A polynomial R-relation valid as the exponent varies differentiates to an inhomogeneous L-relation. The correction coefficients are formal derivatives of the original coefficient polynomials. This is applied to Carlson's homogeneity recurrence, with a single nonzero polynomial family valid for all parameters and slit-plane nodes. It is a concrete instance of Carlson (1987), Theorem 3.1, not yet that theorem for an arbitrary list of associated shifts.

theorem DirichletTransform.polynomial_R_relation_implies_L_relation {ι : Type u_1} [Fintype ι] {κ : Type u_2} (s : Finset κ) (A : κ → MvPolynomial (Option (ι ⊕ ι)) ℂ) (e : κ → ℂ) (B : κ → ι → ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (hrel : ∀ (a : ℂ), ∑ j ∈ s, (MvPolynomial.eval (carlsonRecurrencePoint a b z)) (A j) * regCarlsonRSlit (-a + e j) (B j) z = 0) (a : ℂ) : ∑ j ∈ s, (MvPolynomial.eval (carlsonRecurrencePoint a b z)) (A j) * regCarlsonLSlit (-a + e j) (B j) z = ∑ j ∈ s, (MvPolynomial.eval (carlsonRecurrencePoint a b z)) ((MvPolynomial.pderiv none) (A j)) * regCarlsonRSlit (-a + e j) (B j) z

Differentiation of a parameter-polynomial R-relation. The exponent convention -a + e accounts for the positive sign of the R-correction on the right.

theorem DirichletTransform.sum_carlsonAssociatedRecurrenceJointPolynomial_mul_lSlit {ι : Type u_1} [Fintype ι] (a : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ n ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.eval (carlsonRecurrencePoint a b z)) (carlsonAssociatedRecurrenceJointPolynomial n) * regCarlsonLSlit (-a - ↑n) b z = ∑ n ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.eval (carlsonRecurrencePoint a b z)) ((MvPolynomial.pderiv none) (carlsonAssociatedRecurrenceJointPolynomial n)) * regCarlsonRSlit (-a - ↑n) b z

The L homogeneity recurrence, with explicit polynomial R-correction terms, valid for all complex parameters and all slit-plane nodes, including an empty index type.