Carlson's L-function: entire regularized continuation

The continued L-function is the exponent derivative of the continued R-function. Joint entireness of R proves joint entireness of L, not merely separate existence of derivatives. This establishes the parameter part of Carlson (1987), (2.1), for arbitrary complex Dirichlet parameters. This module retains the original right-half-plane node interface. Carlson.L.SlitContinuation extends it to the full product slit plane and proves joint holomorphy in all arguments.

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

The exponent derivative of the entire regularized R-continuation.

Equations

• DirichletTransform.regCarlsonLContinued t z hz b = deriv (fun (s : ℂ) => DirichletTransform.regCarlsonRContinued s z hz b) t

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

The normalized L-continuation. At poles of Γ(∑ i, b i) this is only Lean's totalized expression; the entire object is regCarlsonLContinued.

Equations

• DirichletTransform.carlsonLContinued t z hz b = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonLContinued t z hz b

theorem DirichletTransform.hasDerivAt_regCarlsonRContinued_L {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : HasDerivAt (fun (s : ℂ) => regCarlsonRContinued s z hz b) (regCarlsonLContinued t z hz b) t

The derivative characterization holds at every complex Dirichlet parameter.

theorem DirichletTransform.analyticOnNhd_regCarlsonLContinued_exponent_parameters {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (p : Option ι → ℂ) => regCarlsonLContinued (p none) z hz fun (i : ι) => p (some i)) Set.univ

Joint entireness in the exponent and the Dirichlet parameters, including nonpositive integral parameters and totals.

theorem DirichletTransform.analyticAt_regCarlsonLContinued_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {b : E → ι → ℂ} {p : E} {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hf : AnalyticAt ℂ f p) (hb : AnalyticAt ℂ b p) : AnalyticAt ℂ (fun (w : E) => regCarlsonLContinued (f w) z hz (b w)) p

Analytic substitutions in the exponent and parameters preserve analyticity.

theorem DirichletTransform.analyticOnNhd_regCarlsonLContinued {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (regCarlsonLContinued t z hz) Set.univ

theorem DirichletTransform.regCarlsonLContinued_eq_integral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonLContinued t z hz b = regCarlsonLIntegral t b z

On the convergence region the continued function equals the power-log integral.

theorem DirichletTransform.isRegCarlsonLContinuation_continued {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : IsRegCarlsonContinuation (carlsonLKernel t) z (regCarlsonLContinued t z hz)

L satisfies the existing general Dirichlet-continuation specification.

theorem DirichletTransform.IsRegCarlsonContinuation.eq_regCarlsonLContinued {ι : Type u_1} [Fintype ι] {t : ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation (carlsonLKernel t) z G) (hz : z ∈ carlsonRVariableDomain) : G = regCarlsonLContinued t z hz

Any entire continuation of the native L-integral is the selected L-function.

theorem DirichletTransform.carlsonLContinued_eq_integral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hb : b ∈ Complex.mvBetaConvergent) : carlsonLContinued t z hz b = carlsonLIntegral t b z