Differentiation of Carlson's Pochhammer numerators

The coordinate derivative identity is first obtained from the native Dirichlet integral. Joint analyticity of the finite Pochhammer sum then extends it to all parameters.

theorem DirichletTransform.analyticOnNhd_carlsonRPolynomialNumerator_joint {ι : Type u_1} [Fintype ι] (n : ℕ) : AnalyticOnNhd ℂ (fun (p : (ι → ℂ) × (ι → ℂ)) => carlsonRPolynomialNumerator n p.1 p.2) Set.univ

The Pochhammer numerator is jointly entire in its parameters and nodes.

theorem DirichletTransform.carlsonPartialDeriv_carlsonRPolynomialNumerator_succ {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b z : ι → ℂ) : carlsonPartialDeriv i (carlsonRPolynomialNumerator (n + 1) b) z = (↑n + 1) * b i * carlsonRPolynomialNumerator n (addDirichletUnit b i) z

Differentiating a node lowers the degree and raises the corresponding parameter. The numerator formulation has no exceptional-parameter exclusions.

theorem DirichletTransform.hasDerivAt_carlsonRPolynomialNumerator_update_succ {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b z : ι → ℂ) : HasDerivAt (fun (w : ℂ) => carlsonRPolynomialNumerator (n + 1) b (Function.update z i w)) ((↑n + 1) * b i * carlsonRPolynomialNumerator n (addDirichletUnit b i) z) (z i)

Derivative form of the coordinate differentiation identity.