Carlson's R-polynomials

noncomputable def DirichletTransform.regCarlsonRPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) : ℂ

The entire regularized Carlson polynomial Rₙ(b,z) / Γ(∑ i, b i).

Equations

• DirichletTransform.regCarlsonRPolynomial n b z = DirichletTransform.regDirichletMvPolynomialTransform (DirichletTransform.carlsonPowerPolynomial n z) b

@[reducible, inline]

noncomputable abbrev DirichletTransform.regCarlsonR {ι : Type u_1} [Fintype ι] (n : ℕ) (z b : ι → ℂ) : ℂ

Compatibility spelling using the argument order of the original implementation.

Equations

• DirichletTransform.regCarlsonR n z b = DirichletTransform.regCarlsonRPolynomial n b z

theorem DirichletTransform.regCarlsonDirichletAverage_pow {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : (regCarlsonDirichletAverage b z fun (w : ℂ) => w ^ n) = regCarlsonR n z b

On the ordinary convergence region, the regularized Carlson polynomial agrees with the native Dirichlet average of the corresponding power.

theorem DirichletTransform.differentiable_regCarlsonR {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) : Differentiable ℂ (regCarlsonR n z)

For fixed degree and Carlson variables, the regularized Carlson polynomial is entire in the Dirichlet parameters.

theorem DirichletTransform.analyticOnNhd_regCarlsonR {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) : AnalyticOnNhd ℂ (regCarlsonR n z) Set.univ

Analytic form of entire dependence on the Dirichlet parameters.

theorem DirichletTransform.carlsonPowerPolynomial_smul {ι : Type u_1} [Fintype ι] (n : ℕ) (a : ℂ) (z : ι → ℂ) : (carlsonPowerPolynomial n fun (i : ι) => a * z i) = MvPolynomial.C (a ^ n) * carlsonPowerPolynomial n z

The multivariate polynomial kernel defining the Carlson polynomial is homogeneous in its Carlson variables.

theorem DirichletTransform.eval_carlsonPowerPolynomial_affine {ι : Type u_1} [Fintype ι] (n : ℕ) (a t : ℂ) (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : (MvPolynomial.eval fun (i : ι) => ↑(u i)) (carlsonPowerPolynomial n fun (i : ι) => a * z i + t) = (a * carlsonAffineForm z u + t) ^ n

Evaluation of a translated and scaled Carlson power kernel gives the corresponding binomial power.

theorem DirichletTransform.regCarlsonR_smul_of_mem_mvBetaConvergent {ι : Type u_1} [Fintype ι] (n : ℕ) (a : ℂ) (z : ι → ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonR n (fun (i : ι) => a * z i) b = a ^ n * regCarlsonR n z b

Carlson's degree-n regularized R-polynomial is homogeneous in its variables on the native convergence domain. This is the homogeneous-polynomial observation following Definition 5.7-1.

theorem DirichletTransform.regCarlsonR_const {ι : Type u_1} [Fintype ι] (n : ℕ) (w : ℂ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonR n (fun (x : ι) => w) b = w ^ n / Complex.Gamma (∑ i : ι, b i)

The restriction of a regularized R-polynomial to the diagonal, corresponding to Carlson's equation 5.7(3).