Polynomial relations on the full slit domain #
The polynomial coefficients of an associated relation are entire in the nodes. Consequently the same coefficients that work on right-half-plane nodes work on the whole product slit plane. This extends Carlson's relation 8.4-1 and Theorem 8.4-3 without changing their coefficients or introducing parameter exceptions.
The existential coefficients of Theorem 8.4-3 are still chosen for fixed exponent and Dirichlet parameters; no polynomial or analytic dependence of those witnesses on the parameters is claimed.
theorem
DirichletTransform.exists_polynomial_relation_associatedRSlit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
(s : Fin (Fintype.card ι + 1) → CarlsonRAssociatedShift ι)
:
∃ (A : Fin (Fintype.card ι + 1) → MvPolynomial ι ℂ),
(∃ (j : Fin (Fintype.card ι + 1)), A j ≠ 0) ∧ ∀ z ∈ carlsonRSlitDomain,
∑ j : Fin (Fintype.card ι + 1),
(MvPolynomial.eval z) (A j) * regCarlsonRSlit ((s j).exponentValue t) ((s j).parameterValue b) z = 0
Carlson's Theorem 8.4-3 for all complex parameters and slit-plane nodes. Nontriviality is polynomial nontriviality, not a pointwise assertion. The empty index type is included through the existing entire-parameter theorem.