Polynomial Dirichlet transforms

noncomputable def DirichletTransform.mvPochhammer {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (m : ι → ℕ) : ℂ

A shorthand for the product of Pochhammer polynomials associated to a multi-index. Since ι is finite, monomial multi-indices are represented by ordinary functions ι → ℕ; the finitely supported indices used by MvPolynomial coerce to this type.

Equations

• DirichletTransform.mvPochhammer b m = ∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))

noncomputable def DirichletTransform.regDirichletMonomialTransform {ι : Type u_1} [Fintype ι] (m : ι → ℕ) (b : ι → ℂ) : ℂ

The regularized Dirichlet transform of the monomial with multi-index m. This is an entire function of b.

Equations

• DirichletTransform.regDirichletMonomialTransform m b = DirichletTransform.mvPochhammer b m * (Complex.Gamma (∑ i : ι, (b i + ↑(m i))))⁻¹

theorem DirichletTransform.regDirichletMonomialTransform_eq {ι : Type u_1} [Fintype ι] (m : ι → ℕ) (b : ι → ℂ) : regDirichletMonomialTransform m b = (∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))) * (Complex.Gamma (∑ i : ι, (b i + ↑(m i))))⁻¹

The explicit Pochhammer--Gamma formula for the regularized transform of a monomial. This theorem exposes the useful formula while keeping the shorthand mvPochhammer local to this file.

@[simp]

theorem DirichletTransform.regDirichletMonomialTransform_zero {ι : Type u_1} [Fintype ι] (b : ι → ℂ) : regDirichletMonomialTransform (fun (x : ι) => 0) b = (Complex.Gamma (∑ i : ι, b i))⁻¹

The regularized transform of the constant monomial is the reciprocal Gamma factor.

theorem DirichletTransform.regDirichletIntegral_monomial_mul {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (m : ι → ℕ) (f : (ι → ℝ) → ℂ) : (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => (∏ i : ι, ↑(u i) ^ m i) * f u) = mvPochhammer b m * ProbabilityTheory.regDirichletIntegral (fun (i : ι) => b i + ↑(m i)) f

Multiplying an integrand by a monomial shifts its Dirichlet parameters.

theorem DirichletTransform.regDirichletIntegral_monomial {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (m : ι → ℕ) : (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ∏ i : ι, ↑(u i) ^ m i) = regDirichletMonomialTransform m b

On its domain of definition the regularized integral of a monomial equals its explicit Pochhammer--Gamma transform.

noncomputable def DirichletTransform.regDirichletMvPolynomialTransform {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℂ) (b : ι → ℂ) : ℂ

The regDirichletMonomialTransform extended linearly to multivariate polynomials. The finitely supported indices in p.support are coerced to ordinary functions ι → ℕ.

Equations

• DirichletTransform.regDirichletMvPolynomialTransform p b = ∑ m ∈ p.support, p.coeff m * DirichletTransform.regDirichletMonomialTransform (⇑m) b

theorem DirichletTransform.regDirichletIntegral_mvPolynomial {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) (p : MvPolynomial ι ℂ) : (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => (MvPolynomial.eval fun (i : ι) => ↑(u i)) p) = regDirichletMvPolynomialTransform p b

On its domain of definition the regDirichletIntegral of a multivariate polynomial equals its regularized Dirichlet polynomial transform.

theorem DirichletTransform.differentiable_regDirichletMonomialTransform {ι : Type u_1} [Fintype ι] (m : ι → ℕ) : Differentiable ℂ (regDirichletMonomialTransform m)

The regularized Dirichlet monomial transform is entire in all Dirichlet parameters.

theorem DirichletTransform.analyticOnNhd_regDirichletMonomialTransform {ι : Type u_1} [Fintype ι] (m : ι → ℕ) : AnalyticOnNhd ℂ (regDirichletMonomialTransform m) Set.univ

The regularized Dirichlet monomial transform is analytic in all Dirichlet parameters.

theorem DirichletTransform.differentiable_regDirichletMvPolynomialTransform {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℂ) : Differentiable ℂ (regDirichletMvPolynomialTransform p)

The regularized Dirichlet polynomial transform is entire in all Dirichlet parameters.

theorem DirichletTransform.analyticOnNhd_regDirichletMvPolynomialTransform {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℂ) : AnalyticOnNhd ℂ (regDirichletMvPolynomialTransform p) Set.univ

The regularized Dirichlet transform of a multivariate polynomial is analytic in all Dirichlet parameters.