Joint holomorphy and locally uniform S-series convergence

theorem DirichletTransform.hasSumLocallyUniformlyOn_regCarlsonSSeries_joint {ι : Type u_1} [Fintype ι] : HasSumLocallyUniformlyOn (fun (n : ℕ) (q : ι ⊕ ι → ℂ) => (↑n.factorial)⁻¹ * regCarlsonR n (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) (fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Set.univ

The exponential series converges locally uniformly jointly in parameters and nodes. The coordinates Sum.inl i represent parameters and Sum.inr i represent nodes.

theorem DirichletTransform.analyticOnNhd_regCarlsonSSeries_joint {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Set.univ

The continued S-function is jointly entire in parameters and nodes, by locally uniform convergence of the R-polynomial expansion. A sum index encodes the two vectors.

theorem DirichletTransform.analyticOnNhd_regCarlsonSPartialSum_joint {ι : Type u_1} [Fintype ι] (N : ℕ) : AnalyticOnNhd ℂ (fun (q : ι ⊕ ι → ℂ) => regCarlsonSPartialSum N (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Set.univ

Carlson's finite exponential sums are jointly entire in parameters and nodes.

theorem DirichletTransform.tendstoLocallyUniformlyOn_regCarlsonSPartialSum_joint {ι : Type u_1} [Fintype ι] : TendstoLocallyUniformlyOn (fun (N : ℕ) (q : ι ⊕ ι → ℂ) => regCarlsonSPartialSum N (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) (fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Filter.atTop Set.univ

Carlson's partial sums converge locally uniformly jointly in all parameters and nodes.

theorem DirichletTransform.hasSumLocallyUniformlyOn_carlsonIteratedPartialDeriv_regCarlsonSSeries_joint {ι : Type u_1} [Fintype ι] (is : List (ι ⊕ ι)) : HasSumLocallyUniformlyOn (fun (n : ℕ) => carlsonIteratedPartialDeriv is fun (q : ι ⊕ ι → ℂ) => (↑n.factorial)⁻¹ * regCarlsonR n (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) (carlsonIteratedPartialDeriv is fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Set.univ

Arbitrary mixed parameter/node derivatives of the exponential series may be taken term by term, retaining locally uniform convergence.

theorem DirichletTransform.tendstoLocallyUniformlyOn_carlsonIteratedPartialDeriv_regCarlsonSPartialSum_joint {ι : Type u_1} [Fintype ι] (is : List (ι ⊕ ι)) : TendstoLocallyUniformlyOn (fun (N : ℕ) => carlsonIteratedPartialDeriv is fun (q : ι ⊕ ι → ℂ) => regCarlsonSPartialSum N (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) (carlsonIteratedPartialDeriv is fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Filter.atTop Set.univ

All mixed parameter/node derivatives of the partial sums converge locally uniformly.

theorem DirichletTransform.tendstoLocallyUniformlyOn_iteratedFDeriv_regCarlsonSPartialSum_joint {ι : Type u_1} [Fintype ι] (k : ℕ) : TendstoLocallyUniformlyOn (fun (N : ℕ) => iteratedFDeriv ℂ k fun (q : ι ⊕ ι → ℂ) => regCarlsonSPartialSum N (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) (iteratedFDeriv ℂ k fun (q : ι ⊕ ι → ℂ) => regCarlsonSSeries (fun (i : ι) => q (Sum.inr i)) fun (i : ι) => q (Sum.inl i)) Filter.atTop Set.univ

The iterated Fréchet derivatives of the partial sums converge in multilinear operator norm, locally uniformly jointly in the parameters and nodes.

theorem DirichletTransform.analyticOnNhd_regCarlsonSSeries_variables {ι : Type u_1} [Fintype ι] (b : ι → ℂ) : AnalyticOnNhd ℂ (fun (z : ι → ℂ) => regCarlsonSSeries z b) Set.univ

The continued S-function is entire in its node vector.

theorem DirichletTransform.analyticOnNhd_regCarlsonSIntegral_variables {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : AnalyticOnNhd ℂ (regCarlsonSIntegral b) Set.univ

On the native Dirichlet convergence region, the regularized integral is jointly entire in the Carlson variables.