Associated relations and Euler transformation for Carlson's L-function #
Carlson (1987), (3.1), (3.2), (3.4), and (2.6), in regularized form. All Dirichlet parameters and exponents are arbitrary complex numbers. In particular, the inhomogeneous lowering relation requires no division by a parameter or exponent. The proofs differentiate the corresponding R-identities.
theorem
DirichletTransform.regCarlsonLContinued_eq_sum_addDirichletUnit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRVariableDomain)
:
Equation (3.1), after Gamma regularization.
theorem
DirichletTransform.regCarlsonLContinued_add_one_eq_sum_mul_addDirichletUnit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRVariableDomain)
:
regCarlsonLContinued (t + 1) z hz b = ∑ i : ι, b i * z i * regCarlsonLContinued t z hz (addDirichletUnit b i)
Equation (3.2), after Gamma regularization.
theorem
DirichletTransform.regCarlsonLContinued_eq_addDirichletUnit
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRVariableDomain)
(i : ι)
:
regCarlsonLContinued t z hz b = (∑ j : ι, b j + t) * regCarlsonLContinued t z hz (addDirichletUnit b i) - t * z i * regCarlsonLContinued (t - 1) z hz (addDirichletUnit b i) + regCarlsonRContinued t z hz (addDirichletUnit b i) - z i * regCarlsonRContinued (t - 1) z hz (addDirichletUnit b i)
Equation (3.4), with parameters raised instead of lowered. The two R-terms are essential: L is not homogeneous in the exponent-dependent coefficients.
theorem
DirichletTransform.regCarlsonLContinued_euler
{ι : Type u_1}
[Fintype ι]
(t : ℂ)
(b : ι → ℂ)
{z : ι → ℂ}
(hz : z ∈ carlsonRVariableDomain)
:
regCarlsonLContinued t z hz b = (-∏ i : ι, z i ^ (-b i)) * regCarlsonLContinued (-∑ i : ι, b i - t) (fun (i : ι) => (z i)⁻¹) ⋯ b
Equation (2.6): the Euler transformation for L has a minus sign from the reflected exponent. It holds for all complex Dirichlet parameters after regularization.