The binomial theorem for Carlson's R-polynomials #
Home for Carlson's Section 6.4 and its differential-difference consequences.
The underlying Chu–Vandermonde identity for ascPochhammer is ascPochhammer_eval_add in
Pochhammer.Vandermonde.
theorem
DirichletTransform.regCarlsonR_add_const_of_mem_mvBetaConvergent
{ι : Type u_1}
[Fintype ι]
(n : ℕ)
(a : ℂ)
(z : ι → ℂ)
{b : ι → ℂ}
(hb : b ∈ Complex.mvBetaConvergent)
:
regCarlsonR n (fun (i : ι) => z i + a) b = ∑ m ∈ Finset.range (n + 1), ↑(n.choose m) * a ^ (n - m) * regCarlsonR m z b
Carlson's binomial translation formula for R-polynomials on the native convergence domain; this is the polynomial identity in [Carl77, Section 6.4].
theorem
DirichletTransform.regCarlsonR_add_const
{ι : Type u_1}
[Fintype ι]
(n : ℕ)
(a : ℂ)
(z b : ι → ℂ)
:
regCarlsonR n (fun (i : ι) => z i + a) b = ∑ m ∈ Finset.range (n + 1), ↑(n.choose m) * a ^ (n - m) * regCarlsonR m z b
Carlson's binomial translation identity on the full parameter space. Gamma regularization removes every exclusion on the total parameter.