Reduction of integral exponent shifts to a finite polynomial span

theorem DirichletTransform.carlsonAssociatedRecurrencePolynomial_lower_ne_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] {t : ℂ} (ht : IsCarlsonGammaRegular (1 - t)) (b z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain) (m : ℕ) : (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial (Fintype.card ι) (-t + ↑m) (∑ i : ι, b i + t - ↑m) b) ≠ 0

The last polynomial recurrence coefficient can be used to lower the exponent at every downward step. Unlike the quotient presentation, this statement includes a = 0.

theorem DirichletTransform.carlsonAssociatedRecurrencePolynomial_raise_ne_zero {ι : Type u_1} [Fintype ι] {t : ℂ} (b z : ι → ℂ) (ht : IsCarlsonGammaRegular (∑ i : ι, b i + t - ↑(Fintype.card ι) + 2)) (m : ℕ) : (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial 0 (-(t + ↑m + 1)) (∑ i : ι, b i + t + ↑m + 1) b) ≠ 0

The first polynomial recurrence coefficient can be used to raise the exponent at every upward step. The second regularity hypothesis of Carlson's reduction lemma is exactly the one needed here.

theorem DirichletTransform.exists_polynomial_carlsonAssociated_exponent_reduction {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) (n : ℤ) (hb : b ∈ Complex.mvBetaConvergent) (ht : IsCarlsonGammaRegular (1 - t)) (hct : IsCarlsonGammaRegular (∑ i : ι, b i + t - ↑(Fintype.card ι) + 2)) : ∃ (d : MvPolynomial ι ℂ), d ≠ 0 ∧ ∃ (p : Fin (Fintype.card ι) → MvPolynomial ι ℂ), ∀ z ∈ carlsonRVariableDomain, (MvPolynomial.eval z) d * carlsonRIntegral (t + ↑n) b z = ∑ j : Fin (Fintype.card ι), (MvPolynomial.eval z) (p j) * carlsonRIntegral (t - ↑↑j) b z

Denominator-cleared exponent reduction. The identity holds on the whole variable domain, including the zero set of the denominator polynomial.

theorem DirichletTransform.exists_rational_carlsonAssociated_exponent_reduction {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) (n : ℤ) (hb : b ∈ Complex.mvBetaConvergent) (ht : IsCarlsonGammaRegular (1 - t)) (hct : IsCarlsonGammaRegular (∑ i : ι, b i + t - ↑(Fintype.card ι) + 2)) : ∃ (q : Fin (Fintype.card ι) → CarlsonRRationalCoefficient ι), ∀ z ∈ carlsonRVariableDomain, (∀ (j : Fin (Fintype.card ι)), (MvPolynomial.eval z) (q j).denominator ≠ 0) → carlsonRIntegral (t + ↑n) b z = ∑ j : Fin (Fintype.card ι), (q j).eval z * carlsonRIntegral (t - ↑↑j) b z

Carlson's reduction lemma 8.4-2: all integral exponent shifts with fixed parameters lie in the rational-function span of card ι consecutive R-functions.