Carlson's L-function: native integrals

The kernel is w ^ t * log w, with the principal complex logarithm. These native integrals are distinguished from their analytic continuations in b.

References

• B. C. Carlson, Dirichlet averages of x^t log x, SIAM J. Math. Anal. 18 (1987), 550–565, equations (1.2), (1.3), (2.2), and (2.4).

noncomputable def DirichletTransform.carlsonLKernel (t w : ℂ) : ℂ

The power-logarithm kernel whose Dirichlet average is Carlson's L_t.

Equations

• DirichletTransform.carlsonLKernel t w = w ^ t * Complex.log w

noncomputable def DirichletTransform.regCarlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) : ℂ

The native regularized L_t / Γ(∑ i, b i) integral.

Equations

• DirichletTransform.regCarlsonLIntegral t b z = DirichletTransform.regCarlsonDirichletAverage b z (DirichletTransform.carlsonLKernel t)

noncomputable def DirichletTransform.carlsonLIntegral {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) : ℂ

Carlson's native normalized L-integral.

Equations

• DirichletTransform.carlsonLIntegral t b z = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonLIntegral t b z

theorem DirichletTransform.hasDerivAt_regCarlsonRIntegral_L {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => regCarlsonRIntegral s b z) (regCarlsonLIntegral t b z) t

Equation (1.2): differentiating the native R-integral inserts the logarithm.

theorem DirichletTransform.hasDerivAt_carlsonRIntegral_L {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => carlsonRIntegral s b z) (carlsonLIntegral t b z) t

theorem DirichletTransform.analyticOnNhd_regCarlsonLIntegral_exponent {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (t : ℂ) => regCarlsonLIntegral t b z) Set.univ

The native L-integral is entire in its exponent on the convergence region.

theorem DirichletTransform.regCarlsonLIntegral_perm {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) (σ : Equiv.Perm ι) : regCarlsonLIntegral t (b ∘ ⇑σ) (z ∘ ⇑σ) = regCarlsonLIntegral t b z

Equation (2.2), for the native regularized integral.