Polynomial recurrences on the full slit domain

theorem DirichletTransform.polynomial_relation_regCarlsonRSlit_of_right {ι : Type u_1} [Fintype ι] {κ : Type u_2} (s : Finset κ) (A : κ → MvPolynomial ι ℂ) (t : κ → ℂ) (b : κ → ι → ℂ) (h : ∀ (z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain), ∑ j ∈ s, (MvPolynomial.eval z) (A j) * regCarlsonRContinued (t j) z hz (b j) = 0) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ j ∈ s, (MvPolynomial.eval z) (A j) * regCarlsonRSlit (t j) (b j) z = 0

A finite polynomial-coefficient relation extends with its original coefficients.

theorem DirichletTransform.sum_carlsonAssociatedRecurrencePolynomial_mul_rSlit {ι : Type u_1} [Fintype ι] [Nonempty ι] (a : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ n ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n a (∑ i : ι, b i - a) b) * regCarlsonRSlit (-a - ↑n) b z = 0

Relation 8.4-1, with its polynomial coefficients, on the full slit domain.