Associated shifts and rational coefficient data

structure DirichletTransform.CarlsonRAssociatedShift (ι : Type u_2) : Type u_2

Integral shifts specifying a Carlson R-function associated to a fixed exponent and Dirichlet parameter vector.

• exponent : ℤ

  Integral shift of the homogeneity parameter.

• parameter : ι → ℤ

  Integral shifts of the Dirichlet parameters.

def DirichletTransform.CarlsonRAssociatedShift.exponentValue {ι : Type u_1} (s : CarlsonRAssociatedShift ι) (t : ℂ) : ℂ

Apply an associated shift to an R-function's exponent.

Equations

• s.exponentValue t = t + ↑s.exponent

def DirichletTransform.CarlsonRAssociatedShift.parameterValue {ι : Type u_1} (s : CarlsonRAssociatedShift ι) (b : ι → ℂ) : ι → ℂ

Apply an associated shift to an R-function's Dirichlet parameters.

Equations

• s.parameterValue b i = b i + ↑(s.parameter i)

structure DirichletTransform.CarlsonRRationalCoefficient (ι : Type u_2) : Type u_2

A rational function in the Carlson variables, represented by a numerator and a nonzero denominator polynomial.

• numerator : MvPolynomial ι ℂ

  Numerator polynomial.

• denominator : MvPolynomial ι ℂ

  Denominator polynomial.

• denominator_ne_zero : self.denominator ≠ 0

  The denominator is not the zero polynomial.

noncomputable def DirichletTransform.CarlsonRRationalCoefficient.eval {ι : Type u_1} (q : CarlsonRRationalCoefficient ι) (z : ι → ℂ) : ℂ

Evaluate a rational Carlson coefficient away from the zero set of its denominator.

Equations

• q.eval z = (MvPolynomial.eval z) q.numerator / (MvPolynomial.eval z) q.denominator