Universal polynomial recurrence coefficients and specialization

The coordinates are none for the exponent parameter, some (inl i) for Dirichlet parameters and some (inr i) for nodes. No R-function dependence or recurrence theorem is imported here.

def DirichletTransform.carlsonRecurrencePoint {ι : Type u_1} (a : ℂ) (b z : ι → ℂ) : Option (ι ⊕ ι) → ℂ

Coordinates for a polynomial in the exponent parameter, Dirichlet parameters, and nodes.

Equations

• DirichletTransform.carlsonRecurrencePoint a b z i = i.elim a (Sum.elim b z)

noncomputable def DirichletTransform.recurrencePochhammer {ι : Type u_1} (n : ℕ) (p : MvPolynomial (Option (ι ⊕ ι)) ℂ) : MvPolynomial (Option (ι ⊕ ι)) ℂ

Substitute a joint parameter polynomial into an ascending Pochhammer polynomial.

Equations

• DirichletTransform.recurrencePochhammer n p = Polynomial.eval₂ MvPolynomial.C p (ascPochhammer ℂ n)

noncomputable def DirichletTransform.carlsonAssociatedRecurrenceJointPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) : MvPolynomial (Option (ι ⊕ ι)) ℂ

The coefficient of R_{-a-n} as one polynomial in all parameters and nodes.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.eval_carlsonAssociatedRecurrenceJointPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (a : ℂ) (b z : ι → ℂ) : (MvPolynomial.eval (carlsonRecurrencePoint a b z)) (carlsonAssociatedRecurrenceJointPolynomial n) = (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n a (∑ i : ι, b i - a) b)

Specialization recovers the existing division-free recurrence coefficients.

theorem DirichletTransform.carlsonAssociatedRecurrenceJointPolynomial_zero_ne_zero {ι : Type u_1} [Fintype ι] : carlsonAssociatedRecurrenceJointPolynomial 0 ≠ 0

The universal family is not the zero polynomial family. This is polynomial nontriviality; specializations may still have vanishing coefficients.

theorem DirichletTransform.hasDerivAt_carlsonRecurrencePoint_eval {ι : Type u_1} (p : MvPolynomial (Option (ι ⊕ ι)) ℂ) (a : ℂ) (b z : ι → ℂ) : HasDerivAt (fun (s : ℂ) => (MvPolynomial.eval (carlsonRecurrencePoint s b z)) p) ((MvPolynomial.eval (carlsonRecurrencePoint a b z)) ((MvPolynomial.pderiv none) p)) a

Formal differentiation supplies a polynomial coefficient derivative, including at exceptional parameter values.