Zero-parameter deletion for the continued R-function

Every finite set of right-half-plane nodes fits in a disk of holomorphy of the principal power. Carlson's continued Taylor formula therefore deletes a zero parameter for every complex exponent and every remaining parameter vector.

theorem DirichletTransform.exists_carlsonR_center {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : ∃ (A : ℝ), 0 < A ∧ ‖fun (i : ι) => z i - ↑A‖ < A

A finite right-half-plane node vector lies in a disk centered on the positive real axis whose open disk is contained in the right half-plane.

theorem DirichletTransform.analyticOnNhd_cpow_carlsonR_center (t : ℂ) (A : ℝ) : AnalyticOnNhd ℂ (fun (w : ℂ) => w ^ t) (Metric.ball (↑A) A)

The principal power is holomorphic on any disk centered at a positive real number with that number as radius.

theorem DirichletTransform.regCarlsonRContinued_option_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (t : ℂ) {b : Option ι → ℂ} (hb : b none = 0) {z : Option ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued t z hz b = regCarlsonRContinued t (z ∘ some) ⋯ (b ∘ some)

Carlson's zero-parameter deletion for the general continued R-function. The exponent and remaining Dirichlet parameters are arbitrary complex numbers.