Equal-node aggregation for Carlson functions #
These specializations of the general continuation theorem impose no restrictions
on the Dirichlet parameters. The R function retains its right-half-plane node
domain; the polynomial and S statements allow arbitrary complex nodes.
theorem
DirichletTransform.regCarlsonRContinued_aggregate
{ι : Type u_1}
{κ : Type u_2}
[Fintype ι]
[Fintype κ]
{q : ι → κ}
(hq : Function.Surjective q)
(t : ℂ)
{z : κ → ℂ}
(hz : z ∈ carlsonRVariableDomain)
(b : ι → ℂ)
:
Equal-node aggregation for the entire regularized R function.
theorem
DirichletTransform.regCarlsonR_aggregate
{ι : Type u_1}
{κ : Type u_2}
[Fintype ι]
[Fintype κ]
{q : ι → κ}
(hq : Function.Surjective q)
(n : ℕ)
(z : κ → ℂ)
(b : ι → ℂ)
:
Equal-node aggregation for regularized R polynomials at every complex parameter.
theorem
DirichletTransform.regCarlsonSSeries_aggregate
{ι : Type u_1}
{κ : Type u_2}
[Fintype ι]
[Fintype κ]
{q : ι → κ}
(hq : Function.Surjective q)
(z : κ → ℂ)
(b : ι → ℂ)
:
Equal-node aggregation for the entire regularized S function.