The Dirichlet or Simplex Mellin transform

By the regularized Dirichlet transform we understand the transformation from a complex-valued function $f$ on the standard simplex $E^{k-1}$ (embedded in $ℝ^k$) to an analytic function of $b∈ℂ^k$ that is the analytic continuation of regDirichletIntegral b f.

Terminology here is provisional. We are using the name (regularized) Dirichlet transform because it is the central transform in Carlson's theory of Dirichlet averages. However, the name (regularized) simplex Mellin transform is also appropriate.

Main definitions and results

• dirichletConvergenceRegion: the parameter region re (b i) > -N.
• exists_regDirichletContinuation_of_contDiffNear: (card ι - 1) * N derivatives give analytic continuation to the region re (b i) > -N.
• exists_entire_regDirichletContinuation_of_contDiffNear: smoothness to every finite order gives an entire continuation.

Polynomial transforms are developed in Dirichlet.Polynomial; smooth simplex functions, tangential derivatives, and face restrictions are developed in StdSimplexMeasure.Smooth. Dirichlet.Transform.Parametric retains holomorphic auxiliary parameters throughout the finite-shift construction and gluing. The shared shift-region and power-partition lemmas are exported here for that construction.

References

[Carl77] Carlson, Bille Chandler. "Special functions of applied mathematics." Academic Press, 1977.

Finite-order analytic continuation

def DirichletTransform.dirichletConvergenceRegion {ι : Type u_1} (N : ℕ) : Set (ι → ℂ)

The region of Dirichlet parameters satisfying -N < re (b i) in every coordinate.

Equations

• DirichletTransform.dirichletConvergenceRegion N = {b : ι → ℂ | ∀ (i : ι), -↑N < (b i).re}

theorem DirichletTransform.isOpen_dirichletConvergenceRegion {ι : Type u_1} [Finite ι] (N : ℕ) : IsOpen (dirichletConvergenceRegion N)

Dirichlet convergence regions are open.

@[simp]

theorem DirichletTransform.dirichletConvergenceRegion_zero {ι : Type u_1} : dirichletConvergenceRegion 0 = Complex.mvBetaConvergent

The order-zero convergence region is the ordinary domain of absolute convergence.

theorem DirichletTransform.dirichletConvergenceRegion_mono {ι : Type u_1} {N M : ℕ} (hNM : N ≤ M) : dirichletConvergenceRegion N ⊆ dirichletConvergenceRegion M

Increasing the available regularity enlarges the corresponding convergence region.

theorem DirichletTransform.mvBetaConvergent_subset_dirichletConvergenceRegion {ι : Type u_1} (N : ℕ) : Complex.mvBetaConvergent ⊆ dirichletConvergenceRegion N

The ordinary convergence region is contained in every finite-order continuation region.

theorem DirichletTransform.exists_regDirichletContinuation_of_unique {ι : Type u_1} [Fintype ι] [Unique ι] {f : (ι → ℝ) → ℂ} (_hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : ∃ (F : (ι → ℂ) → ℂ), AnalyticOn ℂ F Set.univ ∧ Set.EqOn F (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b f) Complex.mvBetaConvergent

On a singleton index type the regularized Dirichlet integral is f 1 / Gamma b, hence entire in the Dirichlet parameter.

theorem DirichletTransform.exists_regDirichletContinuation_of_isEmpty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (f : (ι → ℝ) → ℂ) : ∃ (F : (ι → ℂ) → ℂ), AnalyticOn ℂ F Set.univ ∧ Set.EqOn F (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b f) Complex.mvBetaConvergent

The empty-index integral is identically zero, hence entire.

theorem DirichletTransform.exists_regDirichletContinuation_zero {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex 0 f) : ∃ (F : (ι → ℂ) → ℂ), AnalyticOn ℂ F (dirichletConvergenceRegion 0) ∧ Set.EqOn F (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b f) Complex.mvBetaConvergent

At order zero, the native regularized Dirichlet integral itself supplies the analytic function on the ordinary convergence region.

theorem DirichletTransform.isPreconnected_dirichletConvergenceRegion {ι : Type u_1} (N : ℕ) : IsPreconnected (dirichletConvergenceRegion N)

Dirichlet continuation regions are convex, hence preconnected.

theorem DirichletTransform.eqOn_dirichletContinuation {ι : Type u_1} [Fintype ι] {N : ℕ} {F G : (ι → ℂ) → ℂ} (hF : AnalyticOn ℂ F (dirichletConvergenceRegion N)) (hG : AnalyticOn ℂ G (dirichletConvergenceRegion N)) (hEq : Set.EqOn F G Complex.mvBetaConvergent) : Set.EqOn F G (dirichletConvergenceRegion N)

Two analytic continuations to a Dirichlet convergence region that agree on the ordinary convergence region agree everywhere on the continuation region.

theorem DirichletTransform.slice_jacobian_exponent {ι : Type u_1} [Fintype ι] (i : ι) [Nontrivial ι] (b : ι → ℂ) : ↑(Fintype.card ι - 2) + ∑ q : { j : ι // j ≠ i }, (b ↑q - 1) = ∑ q : { j : ι // j ≠ i }, b ↑q - 1

Jacobian identity for the complementary-coordinate exponent in a simplex slice.

theorem DirichletTransform.regDirichletIntegral_split_at {ι : Type u_1} [Fintype ι] [Nontrivial ι] (i : ι) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : ProbabilityTheory.regDirichletIntegral b f = (b i).regIncompleteMellin 1 fun (t : ℝ) => (1 - ↑t) ^ (∑ q : { j : ι // j ≠ i }, b ↑q - 1) * ProbabilityTheory.regDirichletIntegral (fun (q : { j : ι // j ≠ i }) => b ↑q) (stdSimplexSlice i t f)

Native slice formula: a regularized Dirichlet integral is an incomplete Mellin transform in one coordinate of a complementary regularized Dirichlet integral on the opposite face.

Continuation by tangential integration by parts

def DirichletTransform.shiftRegion {ι : Type u_1} (i : ι) (l : List { j : ι // j ≠ i }) : Set (ι → ℂ)

Convergence region for a finite list of tangential parameter shifts.

Equations

• DirichletTransform.shiftRegion i l = {b : ι → ℂ | ↑l.length < (b i).re ∧ ∀ (j : { j : ι // j ≠ i }), 0 < (b ↑j).re + ↑(List.count j l)}

theorem DirichletTransform.shiftRegion_cons {ι : Type u_1} (i : ι) (j : { j : ι // j ≠ i }) (l : List { j : ι // j ≠ i }) {b : ι → ℂ} (hb : b ∈ shiftRegion i (j :: l)) : b + Pi.single (↑j) 1 - Pi.single i 1 ∈ shiftRegion i l ∧ b + Pi.single (↑j) 1 ∈ shiftRegion i l

noncomputable def DirichletTransform.shiftList {ι : Type u_1} [Fintype ι] (i : ι) (N : ℕ) : List { j : ι // j ≠ i }

Each free coordinate is shifted N times.

Equations

• DirichletTransform.shiftList i N = (List.replicate N Finset.univ.toList).flatten

theorem DirichletTransform.shiftList_length {ι : Type u_1} [Fintype ι] (i : ι) (N : ℕ) : (shiftList i N).length = (Fintype.card ι - 1) * N

theorem DirichletTransform.shiftList_count {ι : Type u_1} [Fintype ι] (i : ι) (N : ℕ) (j : { j : ι // j ≠ i }) : List.count j (shiftList i N) = N

theorem DirichletTransform.regDirichletIntegral_power_partition {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) (M : ℕ) : ProbabilityTheory.regDirichletIntegral b f = ∑ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ M) * ProbabilityTheory.regDirichletIntegral (b + Pi.single i ↑M) fun (u : ι → ℝ) => f u / powerPartitionDenom M u

theorem DirichletTransform.exists_regDirichletContinuation_of_contDiffNear {ι : Type u_1} [Fintype ι] {N : ℕ} {f : (ι → ℝ) → ℂ} (hf : ContDiffNearStdSimplex ((Fintype.card ι - 1) * N) f) : ∃ (F : (ι → ℂ) → ℂ), AnalyticOn ℂ F (dirichletConvergenceRegion N) ∧ Set.EqOn F (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b f) Complex.mvBetaConvergent

If f has (card ι - 1) * N continuous derivatives near the closed simplex, its regularized Dirichlet integral continues to -N < re (b i) for every i.

The dimension factor is essential: the former statement with only N derivatives was false at intersecting faces. The proof uses N tangential integrations by parts in each of the card ι - 1 free coordinates.

theorem DirichletTransform.exists_entire_regDirichletContinuation_of_contDiffNear {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℂ} (hf : ∀ (N : ℕ), ContDiffNearStdSimplex N f) : ∃ (F : (ι → ℂ) → ℂ), AnalyticOnNhd ℂ F Set.univ ∧ Set.EqOn F (fun (b : ι → ℂ) => ProbabilityTheory.regDirichletIntegral b f) Complex.mvBetaConvergent

If a simplex function has every finite order of differentiability on a neighborhood of the simplex, its compatible finite-order regularized continuations glue to an entire function of all Dirichlet parameters.