Generating functions of Carlson's R-polynomials

This file develops [Carl77, Section 6.6]. The scalar binomial series ∑ (a)_n t^n / n! = (1-t)^{-a} is Complex.hasSum_ascPochhammer_mul_pow_div_factorial in Pochhammer.BinomialSeries.

noncomputable def DirichletTransform.carlsonGeneratingCoeff {ι : Type u_1} (s : Finset ι) (b z : ι → ℂ) (n : ℕ) : ℂ

The Pochhammer-weighted multinomial coefficient of total degree n on a finite index set.

Equations

• DirichletTransform.carlsonGeneratingCoeff s b z n = ∑ m ∈ s.piAntidiag n, (↑(Nat.multinomial s m) * ∏ i ∈ s, z i ^ m i) * ∏ i ∈ s, Polynomial.eval (b i) (ascPochhammer ℂ (m i))

theorem DirichletTransform.carlsonRPolynomialNumerator_eq_sum_piAntidiag {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) : carlsonRPolynomialNumerator n b z = carlsonGeneratingCoeff Finset.univ b z n

The Pochhammer numerator is the complete degree-n multinomial expansion.

noncomputable def DirichletTransform.carlsonRGeneratingKernel {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (t : ℂ) : ℂ

The finite product on the left side of Carlson's generating relation 6.6-1.

Equations

• DirichletTransform.carlsonRGeneratingKernel b z t = ∏ i : ι, 1 / (1 - t * z i) ^ b i

theorem DirichletTransform.carlsonGeneratingCoeff_cons_antidiag {ι : Type u_1} {s : Finset ι} {i : ι} (hi : i ∉ s) (b z : ι → ℂ) (t : ℂ) {k l n : ℕ} (hkl : k + l = n) : ∑ m ∈ s.piAntidiag l, ((↑(Nat.multinomial (Finset.cons i s hi) (m + fun (j : ι) => if j = i then k else 0)) * ∏ j ∈ Finset.cons i s hi, z j ^ (m j + if j = i then k else 0)) * ∏ j ∈ Finset.cons i s hi, Polynomial.eval (b j) (ascPochhammer ℂ (m j + if j = i then k else 0))) / ↑n.factorial * t ^ n = Polynomial.eval (b i) (ascPochhammer ℂ k) / ↑k.factorial * (t * z i) ^ k * (carlsonGeneratingCoeff s b z l / ↑l.factorial * t ^ l)

One antidiagonal slice of the Cauchy product for a cons generating coefficient.

theorem DirichletTransform.carlsonGeneratingCoeff_cons {ι : Type u_1} {s : Finset ι} {i : ι} (hi : i ∉ s) (b z : ι → ℂ) (t : ℂ) (n : ℕ) : carlsonGeneratingCoeff (Finset.cons i s hi) b z n / ↑n.factorial * t ^ n = ∑ k ∈ Finset.range (n + 1), Polynomial.eval (b i) (ascPochhammer ℂ k) / ↑k.factorial * (t * z i) ^ k * (carlsonGeneratingCoeff s b z (n - k) / ↑(n - k).factorial * t ^ (n - k))

Adjoining one Carlson coordinate corresponds to the Cauchy product of generating series.

theorem DirichletTransform.carlsonGeneratingCoeff_empty {ι : Type u_1} (b z : ι → ℂ) (n : ℕ) : carlsonGeneratingCoeff ∅ b z n = if n = 0 then 1 else 0

The empty generating series is the constant series 1.

theorem DirichletTransform.hasSum_carlsonGeneratingCoeff {ι : Type u_1} [Finite ι] (s : Finset ι) (b z : ι → ℂ) (t : ℂ) (ht : ∀ i ∈ s, ‖t * z i‖ < 1) : HasSum (fun (n : ℕ) => carlsonGeneratingCoeff s b z n / ↑n.factorial * t ^ n) (∏ i ∈ s, 1 / (1 - t * z i) ^ b i) ∧ Summable fun (n : ℕ) => ‖carlsonGeneratingCoeff s b z n / ↑n.factorial * t ^ n‖

The generating series attached to a subset of the Carlson coordinates.

theorem DirichletTransform.hasSum_carlsonRPolynomialNumerator_div_factorial {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (t : ℂ) (ht : ∀ (i : ι), ‖t * z i‖ < 1) : HasSum (fun (n : ℕ) => carlsonRPolynomialNumerator n b z / ↑n.factorial * t ^ n) (carlsonRGeneratingKernel b z t)

Carlson's generating relation 6.6-1 in the division-free Pochhammer-numerator normalization.

The hypothesis puts every scalar binomial series inside its disk of convergence. The coefficient of t ^ n is the Pochhammer numerator divided by n!; consequently this statement continues to make sense at exceptional values of the total parameter.

theorem DirichletTransform.summable_carlsonRPolynomialNumerator_div_factorial {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (t : ℂ) (ht : ∀ (i : ι), ‖t * z i‖ < 1) : Summable fun (n : ℕ) => carlsonRPolynomialNumerator n b z / ↑n.factorial * t ^ n

Within the common disk ‖t * z i‖ < 1, the series of Carlson numerator coefficients is summable.