Linear transformations of Carlson's R-polynomials

This file contains the algebraic infrastructure for [Carl77, Section 6.5]. The Pochhammer reflection identity used in the book's proof is Complex.ascPochhammer_eval_split_reflection in Pochhammer.Gamma.

theorem DirichletTransform.eval_carlsonPowerPolynomial_smul {ι : Type u_1} [Fintype ι] (n : ℕ) (a : ℂ) (z x : ι → ℂ) : (MvPolynomial.eval x) (carlsonPowerPolynomial n fun (i : ι) => a * z i) = a ^ n * (MvPolynomial.eval x) (carlsonPowerPolynomial n z)

Scaling all Carlson variables scales their degree-n polynomial kernel by a ^ n.

noncomputable def DirichletTransform.carlsonRTransformParameters {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b : ι → ℂ) : ι → ℂ

Carlson's transformed Dirichlet parameters for degree n, with i chosen as the distinguished coordinate in Relation 6.5-3.

Equations

• DirichletTransform.carlsonRTransformParameters n i b = Function.update b i (1 - ∑ j : ι, b j - ↑n)

noncomputable def DirichletTransform.carlsonRTransformVariables {ι : Type u_1} (i : ι) (z : ι → ℂ) : ι → ℂ

Carlson's transformed variables for Relation 6.5-3. The distinguished variable stays fixed and every other variable is replaced by its difference from that variable.

Equations

• DirichletTransform.carlsonRTransformVariables i z j = if j = i then z i else z i - z j

theorem DirichletTransform.sum_carlsonRTransformParameters {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b : ι → ℂ) : ∑ j : ι, carlsonRTransformParameters n i b j = 1 - b i - ↑n

The sum of Carlson's transformed parameters is 1 - b i - n.

theorem DirichletTransform.carlsonRPolynomialNumerator_const {ι : Type u_1} [Fintype ι] (n : ℕ) (b : ι → ℂ) (w : ℂ) : (carlsonRPolynomialNumerator n b fun (x : ι) => w) = Polynomial.eval (∑ i : ι, b i) (ascPochhammer ℂ n) * w ^ n

The Pochhammer numerator of a constant vector of variables is a single Pochhammer symbol, by the multinomial Chu–Vandermonde identity.

theorem DirichletTransform.carlsonRPolynomialNumerator_single {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b : ι → ℂ) (w : ℂ) : carlsonRPolynomialNumerator n b (Pi.single i w) = Polynomial.eval (b i) (ascPochhammer ℂ n) * w ^ n

A numerator with just one nonzero node is a single Pochhammer symbol.

theorem DirichletTransform.carlsonRPolynomialNumerator_transform {ι : Type u_1} [Fintype ι] (n : ℕ) (i : ι) (b z : ι → ℂ) : carlsonRPolynomialNumerator n b z = (-1) ^ n * carlsonRPolynomialNumerator n (carlsonRTransformParameters n i b) (carlsonRTransformVariables i z)

Division-free form of Carlson's multivariate linear transformation 6.5-3.

Using the Pochhammer numerator avoids hypotheses excluding exceptional parameters. Carlson's usual identity follows after division by the relevant total-parameter Pochhammer symbols.

Induction on the degree shows that the difference has zero derivative in every node except the distinguished one. At a constant node vector, Pochhammer reflection makes it zero.