The exponential series and entire parameter continuation of S

def DirichletTransform.IsRegCarlsonSContinuation {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (G : (ι → ℂ) → ℂ) : Prop

A candidate is an entire regularized continuation of Carlson's S if it agrees with the native regularized integral wherever all Dirichlet parameters have positive real part.

Equations

• DirichletTransform.IsRegCarlsonSContinuation z G = DirichletTransform.IsRegCarlsonContinuation Complex.exp z G

theorem DirichletTransform.IsRegCarlsonSContinuation.analyticOnNhd {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonSContinuation z G) : AnalyticOnNhd ℂ G Set.univ

A regularized Carlson S continuation is entire in the Dirichlet parameters.

theorem DirichletTransform.IsRegCarlsonSContinuation.eq_integral {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonSContinuation z G) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : G b = regCarlsonSIntegral b z

A regularized Carlson S continuation agrees with the native integral on its ordinary domain of absolute convergence.

theorem DirichletTransform.IsRegCarlsonSContinuation.eq {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {G H : (ι → ℂ) → ℂ} (hG : IsRegCarlsonSContinuation z G) (hH : IsRegCarlsonSContinuation z H) : G = H

An entire regularized continuation of Carlson's S, if it exists, is unique.

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

The series defining the entire regularized Carlson S function. This is the exponential specialization of Carlson's regularized Taylor construction.

Equations

• DirichletTransform.regCarlsonSSeries z b = DirichletTransform.regCarlsonTaylorSeries 0 (fun (n : ℕ) => (↑n.factorial)⁻¹) z b

theorem DirichletTransform.regCarlsonSSeries_eq_tsum_regCarlsonR {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) : regCarlsonSSeries z b = ∑' (n : ℕ), (↑n.factorial)⁻¹ * regCarlsonR n z b

Carlson's formula (6.3-5), exposing the regularized S continuation as the exponential generating series of the regularized R polynomials.

theorem DirichletTransform.summable_norm_regCarlsonR_div_factorial {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) : Summable fun (n : ℕ) => ‖(↑n.factorial)⁻¹ * regCarlsonR n z b‖

Carlson's exponential series is absolutely summable at every complex parameter and node vector, including parameters outside the native integral's convergence region.

theorem DirichletTransform.hasSum_regCarlsonSSeries {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) : HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ * regCarlsonR n z b) (regCarlsonSSeries z b)

The exponential generating series sums to the continued S function for all complex parameters and nodes, without an integral-convergence hypothesis.

noncomputable def DirichletTransform.regCarlsonSPartialSum {ι : Type u_1} [Fintype ι] (N : ℕ) (z b : ι → ℂ) : ℂ

The Nth partial sum in Carlson's exponential-series construction of the regularized S function.

Equations

• DirichletTransform.regCarlsonSPartialSum N z b = ∑ n ∈ Finset.range N, (↑n.factorial)⁻¹ * DirichletTransform.regCarlsonR n z b

theorem DirichletTransform.analyticOnNhd_regCarlsonSPartialSum {ι : Type u_1} [Fintype ι] (N : ℕ) (z : ι → ℂ) : AnalyticOnNhd ℂ (regCarlsonSPartialSum N z) Set.univ

Every partial sum in Carlson's construction is entire in the Dirichlet parameters.

theorem DirichletTransform.tendsto_regCarlsonSPartialSum {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) (h : Summable fun (n : ℕ) => (↑n.factorial)⁻¹ * regCarlsonR n z b) : Filter.Tendsto (fun (N : ℕ) => regCarlsonSPartialSum N z b) Filter.atTop (nhds (regCarlsonSSeries z b))

The partial-sum consequence of summability. The unconditional version for all complex parameters and nodes is tendsto_regCarlsonSPartialSum_all.

theorem DirichletTransform.tendsto_regCarlsonSPartialSum_all {ι : Type u_1} [Fintype ι] (z b : ι → ℂ) : Filter.Tendsto (fun (N : ℕ) => regCarlsonSPartialSum N z b) Filter.atTop (nhds (regCarlsonSSeries z b))

The partial sums converge to the entire regularized S function at every complex parameter and node vector.

theorem DirichletTransform.hasSum_exp_carlsonAffineForm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) : HasSum (fun (n : ℕ) => carlsonAffineForm z u ^ n / ↑n.factorial) (Complex.exp (carlsonAffineForm z u))

The exponential series of the Carlson affine form converges pointwise to the exponential kernel.

theorem DirichletTransform.hasSum_regCarlsonR_div_factorial_eq_regCarlsonSIntegral {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ * regCarlsonR n z b) (regCarlsonSIntegral b z)

On the native convergence region, Carlson's exponential series is summable and its sum is the regularized S integral. This is the integral form of the power-series construction in Sections 5.7--5.8.

theorem DirichletTransform.summable_regCarlsonR_div_factorial {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : Summable fun (n : ℕ) => (↑n.factorial)⁻¹ * regCarlsonR n z b

Carlson's exponential series is summable throughout the native Dirichlet convergence region.

theorem DirichletTransform.regCarlsonSSeries_eq_regCarlsonSIntegral {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonSSeries z b = regCarlsonSIntegral b z

On the native convergence region, the series construction of the regularized S function agrees with its defining Dirichlet integral.

theorem DirichletTransform.analyticOnNhd_regCarlsonSSeries {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : AnalyticOnNhd ℂ (regCarlsonSSeries z) Set.univ

Carlson's series construction is entire in all Dirichlet parameters. This is the analytic assertion in Corollary 6.3-3; its proof is the locally uniform version of the coefficient estimate used above for pointwise summability.

theorem DirichletTransform.isRegCarlsonSContinuation_series {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : IsRegCarlsonSContinuation z (regCarlsonSSeries z)

The exponential series realizes Carlson's entire regularized continuation of S.

theorem DirichletTransform.IsRegCarlsonSContinuation.eq_series {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonSContinuation z G) : G = regCarlsonSSeries z

Every entire regularized continuation of Carlson's S is the exponential series.