Fixed-parameter recurrence for associated Carlson R-functions

This file contains the coefficient polynomials and recurrence of [Carl77, Relation 8.4-1]. The native-strip proof follows Carlson's pp. 245–246: the single-integral representation from Exercise 6.8-8, integration by parts with justified convergence and endpoint limits, the elementary-symmetric expansion, and beta/Gamma normalization. Analytic continuation then removes the strip restriction. There are no admitted proofs in this file.

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

The division-free, regularized residual of Carlson's fixed-parameter recurrence. The constraint on the total parameter is built into this definition.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.analyticOnNhd_carlsonAssociatedRecurrenceResidual_exponent {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (a : ℂ) => carlsonAssociatedRecurrenceResidual a b z) Set.univ

The division-free recurrence residual is entire in its exponent parameter.

theorem DirichletTransform.analyticOnNhd_carlsonAssociatedRecurrenceResidual_parameters {ι : Type u_1} [Fintype ι] (a : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (fun (b : ι → ℂ) => carlsonAssociatedRecurrenceResidual a b z) Complex.mvBetaConvergent

The same residual is analytic in the Dirichlet parameters on their native domain.

theorem DirichletTransform.carlsonAssociatedRecurrenceResidual_eq_zero_of_strip {ι : Type u_1} [Fintype ι] [Nonempty ι] {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hstrip : ∀ (a : ℂ), ∀ b ∈ Complex.mvBetaConvergent, 0 < a.re → ↑(Fintype.card ι) < (∑ i : ι, b i - a).re → carlsonAssociatedRecurrenceResidual a b z = 0) (a : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : carlsonAssociatedRecurrenceResidual a b z = 0

A proof of the recurrence in the absolutely convergent single-integral strip suffices for all native Dirichlet parameters and all exponents. Analytic continuation is performed first in the exponent, then in the Dirichlet parameters, using division-free coefficients. This lemma does not assume the recurrence outside the strip.

noncomputable def DirichletTransform.carlsonAssociatedRecurrenceKernel {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) (w : ℂ) : ℂ

The primitive whose endpoint values give the associated-function recurrence.

Equations

• DirichletTransform.carlsonAssociatedRecurrenceKernel a b z w = w ^ a * ∏ i : ι, (1 + w * z i) ^ (1 - b i)

theorem DirichletTransform.hasDerivAt_carlsonAssociatedRecurrenceKernel {ι : Type u_1} [Fintype ι] (a : ℂ) (b z : ι → ℂ) {w : ℂ} (hw : w ∈ Complex.slitPlane) (hz : ∀ (i : ι), 1 + w * z i ∈ Complex.slitPlane) : HasDerivAt (carlsonAssociatedRecurrenceKernel a b z) ((w ^ (a - 1) * ∏ i : ι, (1 + w * z i) ^ (-b i)) * (a * ∏ i : ι, (1 + w * z i) + w * ∑ i : ι, (1 - b i) * z i * ∏ j ∈ Finset.univ.erase i, (1 + w * z j))) w

The derivative of the ray primitive, with all complex powers factored out. The remaining factor is a polynomial in w; expanding it gives the elementary symmetric coefficients of Carlson's recurrence.

theorem DirichletTransform.tendsto_carlsonAssociatedRecurrenceKernel_zero {ι : Type u_1} [Fintype ι] {a : ℂ} (ha : 0 < a.re) (b z : ι → ℂ) : Filter.Tendsto (carlsonAssociatedRecurrenceKernel a b z) (nhds 0) (nhds 0)

The left endpoint of the ray primitive vanishes whenever the first Mellin exponent has positive real part. No condition on the other parameters is needed here.

theorem DirichletTransform.hasDerivAt_carlsonAssociatedRecurrenceKernel_ofReal {ι : Type u_1} [Fintype ι] (a : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (r : ℝ) => carlsonAssociatedRecurrenceKernel a b z ↑r) ((↑x ^ (a - 1) * ∏ i : ι, (1 + ↑x * z i) ^ (-b i)) * (a * ∏ i : ι, (1 + ↑x * z i) + ↑x * ∑ i : ι, (1 - b i) * z i * ∏ j ∈ Finset.univ.erase i, (1 + ↑x * z j))) x

On the positive ray, the right-half-plane hypothesis supplies all branch conditions required by the factored derivative formula.

theorem DirichletTransform.tendsto_carlsonAssociatedRecurrenceKernel_atTop {ι : Type u_1} [Fintype ι] {a : ℂ} {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (ha' : ↑(Fintype.card ι) < (∑ i : ι, b i - a).re) : Filter.Tendsto (fun (x : ℝ) => carlsonAssociatedRecurrenceKernel a b z ↑x) Filter.atTop (nhds 0)

The recurrence primitive vanishes at infinity under Carlson's upper strip bound. Unlike the eventual R-function application, this needs no positivity assumption on b.

theorem DirichletTransform.integral_carlsonAssociatedRecurrenceKernel_derivative_eq_zero {ι : Type u_1} [Fintype ι] {a : ℂ} {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (ha : 0 < a.re) (ha' : ↑(Fintype.card ι) < (∑ i : ι, b i - a).re) : ∫ (x : ℝ) in Set.Ioi 0, (↑x ^ (a - 1) * ∏ i : ι, (1 + ↑x * z i) ^ (-b i)) * (a * ∏ i : ι, (1 + ↑x * z i) + ↑x * ∑ i : ι, (1 - b i) * z i * ∏ j ∈ Finset.univ.erase i, (1 + ↑x * z j)) = 0

Carlson's integration-by-parts calculation in the proof of Relation 8.4-1 (pp. 245–246), with absolute integrability and endpoint limits justified.

This is the factored integral identity before expanding the finite products by elementary symmetric polynomials and applying the single-integral representation from Section 6.8.

theorem DirichletTransform.carlsonAssociatedRecurrenceResidual_eq_zero_in_strip {ι : Type u_1} [Fintype ι] [Nonempty ι] {a : ℂ} {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) (ha : 0 < a.re) (ha' : ↑(Fintype.card ι) < (∑ i : ι, b i - a).re) : carlsonAssociatedRecurrenceResidual a b z = 0

The recurrence residual vanishes in the absolutely convergent single-integral strip. Combine the ray integration-by-parts identity with the elementary-symmetric expansion in Carlson's (8.4-5)–(8.4-7), Exercise 6.8-8, and beta/Gamma normalization.

theorem DirichletTransform.carlsonAssociatedRecurrenceResidual_eq_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (a : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : carlsonAssociatedRecurrenceResidual a b z = 0

The division-free residual vanishes for all native Dirichlet parameters and all exponents.

theorem DirichletTransform.sum_carlsonAssociatedRecurrencePolynomial_mul_rIntegral {ι : Type u_1} [Fintype ι] [Nonempty ι] (a : ℂ) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ n ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n a (∑ i : ι, b i - a) b) * carlsonRIntegral (-a - ↑n) b z = 0

Polynomial form of Relation 8.4-1, including the removable-singularity values a = 0 and a' = card ι.

theorem DirichletTransform.sum_carlsonAssociatedRecurrenceCoeff_mul_rIntegral {ι : Type u_1} [Fintype ι] {a a' : ℂ} {b z : ι → ℂ} (hsum : a + a' = ∑ i : ι, b i) (ha : a ≠ 0) (ha' : a' ≠ ↑(Fintype.card ι)) (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonRVariableDomain) : ∑ n ∈ Finset.range (Fintype.card ι + 1), carlsonAssociatedRecurrenceCoeff n a a' b z * carlsonRIntegral (-a - ↑n) b z = 0

Carlson's fixed-parameter recurrence, Relation 8.4-1, on the native domain.