R-polynomial expansions of Carlson's L-function

The scalar Taylor coefficients give an absolutely convergent expansion for all complex Dirichlet parameters, not just the native convergence region. At t = 0 the coefficients are explicit, giving the logarithmic series of Carlson (1987), (5.8), in powers of z - 1 rather than 1 - z.

The derivative-coefficient formulation is nonsingular at integral exponents. Explicit Pochhammer/digamma evaluations at general exponents, (5.3)–(5.7), are not yet supplied by this module.

noncomputable def DirichletTransform.carlsonLCoeff (n : ℕ) (t : ℂ) : ℂ

Scalar Taylor coefficients about one of the power-logarithm kernel.

Equations

• DirichletTransform.carlsonLCoeff n t = iteratedDeriv n (DirichletTransform.carlsonLKernel t) 1 / ↑n.factorial

@[simp]

theorem DirichletTransform.carlsonLCoeff_zero (t : ℂ) : carlsonLCoeff 0 t = 0

The constant coefficient vanishes for every exponent.

@[simp]

theorem DirichletTransform.carlsonLCoeff_one (t : ℂ) : carlsonLCoeff 1 t = 1

The first coefficient is one, independently of the exponent.

theorem DirichletTransform.ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ Complex.slitPlane

The unit disk about one avoids the principal logarithm's branch cut.

theorem DirichletTransform.hasSum_regCarlsonLContinued {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hz1 : ‖fun (i : ι) => z i - 1‖ < 1) : HasSum (fun (n : ℕ) => carlsonLCoeff n t * regCarlsonR n (fun (i : ι) => z i - 1) b) (regCarlsonLContinued t z hz b)

The continued L-function has the R-polynomial Taylor representation on the full unit polydisk, even at exceptional total parameters.

theorem DirichletTransform.summable_norm_regCarlsonLContinued_series {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz1 : ‖fun (i : ι) => z i - 1‖ < 1) : Summable fun (n : ℕ) => ‖carlsonLCoeff n t * regCarlsonR n (fun (i : ι) => z i - 1) b‖

Absolute convergence of the continued L-expansion.

theorem DirichletTransform.carlsonLCoeff_exponent_zero (n : ℕ) : carlsonLCoeff n 0 = -(-1) ^ n / ↑n

At exponent zero the Taylor coefficients are those of log (1 + x).

theorem DirichletTransform.hasSum_regCarlsonLContinued_zero {ι : Type u_1} [Fintype ι] (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hz1 : ‖fun (i : ι) => z i - 1‖ < 1) : HasSum (fun (n : ℕ) => -(-1) ^ n / ↑n * regCarlsonR n (fun (i : ι) => z i - 1) b) (regCarlsonLContinued 0 z hz b)

Equation (5.8), with the sign absorbed into the coefficients of z - 1. The n = 0 term is zero by totalized division.