Documentation

LeanPool.CarlsonFunctions.Carlson.R.SlitAssociated

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.