Node derivatives and translations on the slit domain

The node derivative formula (3.5) of Carlson (1987) extends from the native integral to all complex Dirichlet parameters and all slit-plane nodes. Joint analyticity is essential: it makes the node derivative analytic in the parameters, so permanence of functional relations applies. Summation gives (2.8)–(2.10), including scalar translation, with the inhomogeneous R-term and without convergence restrictions.

theorem DirichletTransform.analyticOnNhd_carlsonPartialDeriv_regCarlsonLSlit_joint {ι : Type u_1} [Fintype ι] (i : ι) : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => carlsonPartialDeriv i (regCarlsonLSlit (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 node derivative is jointly holomorphic in all arguments of L.

theorem DirichletTransform.analyticAt_carlsonPartialDeriv_regCarlsonLSlit_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 (regCarlsonLSlit (t q) (b q)) (z q)) p

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

Carlson (1987), (3.5), on the entire parameter domain and the full node slit domain.

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

Equation (2.9), the translation differential-difference identity.

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

Equation (2.8): the Euler differential identity includes the R-term.

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

Equation (2.10): scalar translation, locally wherever every translated node is in the slit plane. No global translation or branch-crossing assumption is needed.

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

Carlson (1987), (3.6), including the inhomogeneous R-term and all parameter values.