Joint slit-plane continuation: Carlson's Theorem 6.8-2

The regularized function is jointly holomorphic for all complex exponents and Dirichlet parameters and all nodes in the product slit plane. The interval integral supplies the convergent seed; the two associated relations propagate its joint analyticity without division by parameter factors. This proves the continuation assertion of Theorem 6.8-2, but not Carlson's additional contour representation (6.8-7).

theorem DirichletTransform.analyticOnNhd_regCarlsonRSlit_comp {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {U : Set (κ → ℂ)} {t : (κ → ℂ) → ℂ} {b z : (κ → ℂ) → ι → ℂ} (hU : IsOpen U) (ht : AnalyticOnNhd ℂ t U) (hb : AnalyticOnNhd ℂ b U) (hz : AnalyticOnNhd ℂ z U) (hslit : ∀ p ∈ U, z p ∈ carlsonRSlitDomain) : AnalyticOnNhd ℂ (fun (p : κ → ℂ) => regCarlsonRSlit (t p) (b p) (z p)) U

Analytic substitutions in all arguments of the slit-plane continuation. No restrictions are imposed on the exponent or Dirichlet parameters.

theorem DirichletTransform.analyticOnNhd_regCarlsonRSlit_joint {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => regCarlsonRSlit (p none) (fun (i : ι) => p (some (Sum.inl i))) fun (i : ι) => p (some (Sum.inr i))) {p : Option (ι ⊕ ι) → ℂ | (fun (i : ι) => p (some (Sum.inr i))) ∈ carlsonRSlitDomain}

The exponent is none, parameters are some (inl i), and nodes are some (inr i). This is the full joint holomorphy assertion of Carlson's Theorem 6.8-2.

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

At any fixed slit-plane node vector, regularization makes R entire jointly in the exponent and Dirichlet parameters.

theorem DirichletTransform.analyticAt_regCarlsonRSlit_comp {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {t : E → ℂ} {b z : E → ι → ℂ} {p : E} (ht : AnalyticAt ℂ t p) (hb : AnalyticAt ℂ b p) (hz : AnalyticAt ℂ z p) (hslit : z p ∈ carlsonRSlitDomain) : AnalyticAt ℂ (fun (q : E) => regCarlsonRSlit (t q) (b q) (z q)) p

A pointwise composition interface for arbitrary complex normed parameter spaces.

theorem DirichletTransform.analyticAt_carlsonRSlit_comp {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {t : E → ℂ} {b z : E → ι → ℂ} {p : E} (ht : AnalyticAt ℂ t p) (hb : AnalyticAt ℂ b p) (hz : AnalyticAt ℂ z p) (hslit : z p ∈ carlsonRSlitDomain) (hc : ∀ (n : ℕ), ∑ i : ι, b p i ≠ -↑n) : AnalyticAt ℂ (fun (q : E) => carlsonRSlit (t q) (b q) (z q)) p

The ordinary, unregularized function is jointly analytic wherever the total parameter avoids the Gamma poles. The regularized theorem above has no such exclusion.