Reduction of integral Dirichlet parameters

This is the first reduction in Carlson's Section 8.5. A parameter -N can be removed, leaving at most N + 1 functions of one fewer variable. Their exponents are t, t-1, ..., t-N; the coefficients are polynomials in the removed node. All remaining parameters and the exponent are unrestricted.

The lowering relation 8.5(1) is also proved in a form without division, valid at every complex parameter and for coincident nodes as well.

Euler's transformation supplies the complementary terminating case: a polynomial in reciprocal nodes times powers. For integral parameters this is an explicit rational expression.

This reduction does not yet classify all integral or half-integral parameter configurations in terms of elementary functions.

theorem DirichletTransform.exists_polynomial_regCarlsonRContinued_option_neg_nat {ι : Type u_1} [Fintype ι] [Nonempty ι] (N : ℕ) (t : ℂ) {b : Option ι → ℂ} (hb : b none = -↑N) : ∃ (p : Fin (N + 1) → Polynomial ℂ), ∀ (z : Option ι → ℂ) (hz : z ∈ carlsonRVariableDomain), regCarlsonRContinued t z hz b = ∑ j : Fin (N + 1), Polynomial.eval (z none) (p j) * regCarlsonRContinued (t - ↑↑j) (z ∘ some) ⋯ (b ∘ some)

A nonpositive integral parameter can be removed with polynomial coefficients, uniformly in the nodes. This is the raising-and-deletion step in Theorems 8.5-1 and 8.5-3, on the entire regularized parameter domain.

theorem DirichletTransform.regCarlsonRContinued_option_neg_one {ι : Type u_1} [Fintype ι] [Nonempty ι] (t : ℂ) {b : Option ι → ℂ} (hb : b none = -1) {z : Option ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued t z hz b = (∑ i : Option ι, b i + t) * regCarlsonRContinued t (z ∘ some) ⋯ (b ∘ some) - t * z none * regCarlsonRContinued (t - 1) (z ∘ some) ⋯ (b ∘ some)

Explicit removal of the parameter -1, the first nontrivial case of the finite reduction in Section 8.5. No division or node-distinctness is required.

theorem DirichletTransform.regCarlsonRContinued_lower {ι : Type u_1} [Fintype ι] (a : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (i j : ι) : (a - 1) * (z i - z j) * regCarlsonRContinued (-a) z hz b = regCarlsonRContinued (1 - a) z hz (b - Pi.single i 1) - regCarlsonRContinued (1 - a) z hz (b - Pi.single j 1)

Carlson's lowering relation 8.5(1), in pole-free regularized form. It is valid even at a = 1 and coincident nodes, though solving for the left-hand function then requires the usual nonvanishing hypotheses.

theorem DirichletTransform.regCarlsonRContinued_neg_sum_sub_nat {ι : Type u_1} [Fintype ι] (N : ℕ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued (-∑ i : ι, b i - ↑N) z hz b = (∏ i : ι, z i ^ (-b i)) * regCarlsonR N (fun (i : ι) => (z i)⁻¹) b

If the complementary exponent is a nonpositive integer, Euler's transformation reduces the function to a polynomial in reciprocal nodes times complex powers. This is the second terminating case used in Section 8.5.

theorem DirichletTransform.regCarlsonRContinued_neg_sum_sub_nat_int {ι : Type u_1} [Fintype ι] (N : ℕ) (m : ι → ℤ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : (regCarlsonRContinued (-∑ i : ι, ↑(m i) - ↑N) z hz fun (i : ι) => ↑(m i)) = (∏ i : ι, z i ^ (-m i)) * regCarlsonR N (fun (i : ι) => (z i)⁻¹) fun (i : ι) => ↑(m i)

For integral Dirichlet parameters the complementary terminating case is explicitly rational in the nodes: integer powers times a polynomial in their reciprocals. Negative and zero Dirichlet parameters are allowed.