Polynomial dependence of associated Carlson R-functions

This file proves [Carl77, Lemma 8.4-2 and Theorem 8.4-3]. The algebraic exponent reduction uses the recurrence from Carlson.R.AssociatedRecurrence, retaining a denominator-cleared identity valid throughout the variable domain. Repeated parameter raising then reduces associated functions to a common parameter vector. Finite-dimensional linear algebra over the polynomial ring gives a nontrivial polynomial relation between any card ι + 1 of them.

exists_polynomial_relation_associatedRContinued extends this conclusion to arbitrary complex exponents and Dirichlet parameters for the regularized continued functions. The nodes remain in carlsonRVariableDomain (the product of right half-planes).

The choice of common parameters also ensures Gamma regularity at both ends of the exponent recurrence, including the exceptional integral cases discussed by Carlson. The empty index type is handled separately. There are no admitted proofs in this file.

@[instance_reducible]

noncomputable def DirichletTransform.instModuleMvPolynomialComplexForallSubtypeForallMemSetCarlsonRVariableDomain {ι : Type u_1} : Module (MvPolynomial ι ℂ) ({ z : ι → ℂ // z ∈ carlsonRVariableDomain } → ℂ)

Polynomial scalars act by evaluation on the variable domain.

Equations

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

theorem DirichletTransform.exists_polynomial_relation_associatedR {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) (s : Fin (Fintype.card ι + 1) → CarlsonRAssociatedShift ι) (hconv : ∀ (j : Fin (Fintype.card ι + 1)), (s j).parameterValue b ∈ Complex.mvBetaConvergent) : ∃ (A : Fin (Fintype.card ι + 1) → MvPolynomial ι ℂ), (∃ (j : Fin (Fintype.card ι + 1)), A j ≠ 0) ∧ ∀ z ∈ carlsonRVariableDomain, ∑ j : Fin (Fintype.card ι + 1), (MvPolynomial.eval z) (A j) * carlsonRIntegral ((s j).exponentValue t) ((s j).parameterValue b) z = 0

Carlson's existence theorem 8.4-3: any card ι + 1 associated R-functions satisfy a nontrivial homogeneous relation with polynomial coefficients.

theorem DirichletTransform.exists_polynomial_relation_associatedRContinued {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) (s : Fin (Fintype.card ι + 1) → CarlsonRAssociatedShift ι) : ∃ (A : Fin (Fintype.card ι + 1) → MvPolynomial ι ℂ), (∃ (j : Fin (Fintype.card ι + 1)), A j ≠ 0) ∧ ∀ (z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain), ∑ j : Fin (Fintype.card ι + 1), (MvPolynomial.eval z) (A j) * regCarlsonRContinued ((s j).exponentValue t) z hz ((s j).parameterValue b) = 0

Carlson's Theorem 8.4-3 on the entire Dirichlet-parameter space. The relation is nontrivial as a polynomial identity, not merely a pointwise scalar dependence. Gamma regularization includes all exceptional total parameters.