Further associated and differential identities for L

The three-node relation (3.3) and backward-shift relation (3.7) of Carlson (1987) hold for the entire regularized continuation. The translation and Euler differential identities (2.9) and (2.8) are stated for native integrals.

theorem DirichletTransform.isRegCarlsonContinuation_deriv_LKernel {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : IsRegCarlsonContinuation (deriv (carlsonLKernel t)) z fun (b : ι → ℂ) => t * regCarlsonLContinued (t - 1) z hz b + regCarlsonRContinued (t - 1) z hz b

The derivative kernel has an entire continuation expressed through L and R.

theorem DirichletTransform.regCarlsonLContinued_three_node {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i j k : ι) : (z i - z j) * regCarlsonLContinued t z hz (b - Pi.single k 1) + (z j - z k) * regCarlsonLContinued t z hz (b - Pi.single i 1) + (z k - z i) * regCarlsonLContinued t z hz (b - Pi.single j 1) = 0

Equation (3.3), including coincident nodes and indices.

theorem DirichletTransform.regCarlsonLContinued_tangent_sub {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i j : ι) : (z i - z j) * (t * regCarlsonLContinued (t - 1) z hz b + regCarlsonRContinued (t - 1) z hz b) = regCarlsonLContinued t z hz (b - Pi.single j 1) - regCarlsonLContinued t z hz (b - Pi.single i 1)

Equation (3.7), in pole-free regularized form.

theorem DirichletTransform.regCarlsonLIntegral_eq_sum_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonLIntegral t b z = ∑ i : ι, b i * regCarlsonLIntegral t (addDirichletUnit b i) z

The first associated relation on the native convergence region.

theorem DirichletTransform.regCarlsonLIntegral_add_one_eq_sum_mul_addDirichletUnit {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : regCarlsonLIntegral (t + 1) b z = ∑ i : ι, b i * z i * regCarlsonLIntegral t (addDirichletUnit b i) z

The exponent-raising relation on the native convergence region.

theorem DirichletTransform.sum_carlsonPartialDeriv_regCarlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ i : ι, carlsonPartialDeriv i (regCarlsonLIntegral t b) z = t * regCarlsonLIntegral (t - 1) b z + regCarlsonRIntegral (t - 1) b z

Equation (2.9): the differential-difference identity for translations.

theorem DirichletTransform.sum_mul_carlsonPartialDeriv_regCarlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ i : ι, z i * carlsonPartialDeriv i (regCarlsonLIntegral t b) z = t * regCarlsonLIntegral t b z + regCarlsonRIntegral t b z

Equation (2.8): Euler's identity has the inhomogeneous term R.