Differentiation of R on the full slit domain

Carlson's node derivative and the translation and Euler differential identities hold for every complex exponent and Dirichlet parameter vector, and throughout the product slit plane. Joint holomorphy of a node derivative permits continuation first in the parameters, then in the nodes. No L-function theory is used.

theorem DirichletTransform.analyticOnNhd_carlsonPartialDeriv_regCarlsonRSlit_joint {ι : Type u_1} [Fintype ι] (i : ι) : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => carlsonPartialDeriv i (regCarlsonRSlit (p none) fun (j : ι) => p (some (Sum.inl j))) fun (j : ι) => p (some (Sum.inr j))) {p : Option (ι ⊕ ι) → ℂ | (fun (j : ι) => p (some (Sum.inr j))) ∈ carlsonRSlitDomain}

A coordinate derivative of R is jointly holomorphic in all its arguments.

theorem DirichletTransform.analyticAt_carlsonPartialDeriv_regCarlsonRSlit_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {t : E → ℂ} {b z : E → ι → ℂ} {p : E} (ht : AnalyticAt ℂ t p) (hb : AnalyticAt ℂ b p) (hz : AnalyticAt ℂ z p) (hslit : z p ∈ carlsonRSlitDomain) (i : ι) : AnalyticAt ℂ (fun (q : E) => carlsonPartialDeriv i (regCarlsonRSlit (t q) (b q)) (z q)) p

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i : ι) : carlsonPartialDeriv i (regCarlsonRSlit t b) z = t * b i * regCarlsonRSlit (t - 1) (addDirichletUnit b i) z

Relation 5.9-6(9), continued to all complex parameters and slit-plane nodes.

theorem DirichletTransform.hasDerivAt_regCarlsonRSlit_update {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i : ι) : HasDerivAt (fun (w : ℂ) => regCarlsonRSlit t b (Function.update z i w)) (t * b i * regCarlsonRSlit (t - 1) (addDirichletUnit b i) z) (z i)

The first derivative as a one-variable slice, without a convergence hypothesis.

theorem DirichletTransform.carlsonPartialDeriv_carlsonPartialDeriv_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i j : ι) : carlsonPartialDeriv i (carlsonPartialDeriv j (regCarlsonRSlit t b)) z = t * b j * ((t - 1) * addDirichletUnit b j i * regCarlsonRSlit (t - 2) (addDirichletUnit (addDirichletUnit b j) i) z)

Two successive node derivatives on the full slit domain. The shifted coefficient also handles repeated indices, when it is b i + 1 rather than b i.

theorem DirichletTransform.sum_carlsonPartialDeriv_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ i : ι, carlsonPartialDeriv i (regCarlsonRSlit t b) z = t * regCarlsonRSlit (t - 1) b z

The translation differential identity of Theorem 5.9-2 on the full domain.

theorem DirichletTransform.sum_mul_carlsonPartialDeriv_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) : ∑ i : ι, z i * carlsonPartialDeriv i (regCarlsonRSlit t b) z = t * regCarlsonRSlit t b z

Euler's differential identity of Theorem 5.9-2, including the empty index type.

theorem DirichletTransform.hasDerivAt_regCarlsonRSlit_translate {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) {x : ℂ} (hx : (fun (i : ι) => x + z i) ∈ carlsonRSlitDomain) : HasDerivAt (fun (y : ℂ) => regCarlsonRSlit t b fun (i : ι) => y + z i) (t * regCarlsonRSlit (t - 1) b fun (i : ι) => x + z i) x

Scalar translation is differentiable wherever the translated nodes avoid the cut.

theorem DirichletTransform.mul_carlsonPartialDeriv_add_mul_regCarlsonRSlit {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRSlitDomain) (i : ι) : z i * carlsonPartialDeriv i (regCarlsonRSlit t b) z + b i * regCarlsonRSlit t b z = b i * (∑ j : ι, b j + t) * regCarlsonRSlit t (addDirichletUnit b i) z

Relation 5.9-6(10) on the full parameter and slit-node domain.