Analytic continuation of Carlson's Dirichlet averages

This file develops Carlson's regularized Dirichlet average as an entire function of the Dirichlet parameters. It contains the abstract continuation predicate, the polynomial construction, and the native resolvent average. R-polynomial Taylor-series constructions are developed in Carlson.RPolynomial.PowerSeries.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Chapter 6, Academic Press, 1977.

def DirichletTransform.IsRegCarlsonContinuation {ι : Type u_1} [Fintype ι] (f : ℂ → ℂ) (z : ι → ℂ) (G : (ι → ℂ) → ℂ) : Prop

A function of b is a regularized Carlson continuation for f and z if it is entire and agrees with the native regularized Dirichlet integral on its domain of absolute convergence.

Equations

• DirichletTransform.IsRegCarlsonContinuation f z G = (AnalyticOnNhd ℂ G Set.univ ∧ Set.EqOn G (fun (b : ι → ℂ) => DirichletTransform.regCarlsonDirichletAverage b z f) Complex.mvBetaConvergent)

theorem DirichletTransform.IsRegCarlsonContinuation.mk' {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G Set.univ) (hEq : Set.EqOn G (fun (b : ι → ℂ) => regCarlsonDirichletAverage b z f) Complex.mvBetaConvergent) : IsRegCarlsonContinuation f z G

Construct a regularized Carlson continuation from entire dependence on b and agreement with the native integral on the convergence region.

theorem DirichletTransform.IsRegCarlsonContinuation.analyticOnNhd {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) : AnalyticOnNhd ℂ G Set.univ

A regularized Carlson continuation is entire in the Dirichlet parameters.

theorem DirichletTransform.IsRegCarlsonContinuation.eq_native {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : G b = regCarlsonDirichletAverage b z f

A regularized Carlson continuation agrees with the native integral wherever that integral is absolutely convergent.

theorem DirichletTransform.analyticOnNhd_eq_of_eqOn_mvBetaConvergent {ι : Type u_1} [Fintype ι] {G H : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G Set.univ) (hH : AnalyticOnNhd ℂ H Set.univ) (hEq : Set.EqOn G H Complex.mvBetaConvergent) : G = H

Two entire functions of the Dirichlet parameters that agree throughout the ordinary convergence region agree everywhere. This is the common continuation step for the identities proved from Carlson's native integral.

theorem DirichletTransform.IsRegCarlsonContinuation.eq {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G H : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hH : IsRegCarlsonContinuation f z H) : G = H

The entire regularized Carlson continuation, if it exists, is unique.

theorem DirichletTransform.analyticOnNhd_eq_of_eqOn_realDirichletDomain {ι : Type u_1} [Fintype ι] {G H : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G Set.univ) (hH : AnalyticOnNhd ℂ H Set.univ) (hEq : ∀ b ∈ ProbabilityTheory.mvRealBetaDomain, (G fun (i : ι) => ↑(b i)) = H fun (i : ι) => ↑(b i)) : G = H

Two entire candidates which agree for every strictly positive real Dirichlet parameter agree globally. This is the uniqueness principle used to lift probability identities without first proving them on the full complex convergence region.

theorem DirichletTransform.IsRegCarlsonContinuation.mk_of_eqOn_realDirichletDomain {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {z : ι → ℂ} {G H : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G Set.univ) (hH : IsRegCarlsonContinuation f z H) (hEq : ∀ b ∈ ProbabilityTheory.mvRealBetaDomain, (G fun (i : ι) => ↑(b i)) = H fun (i : ι) => ↑(b i)) : IsRegCarlsonContinuation f z G

An entire candidate can be recognized as a Carlson continuation by comparison on positive real parameters with any already established continuation.

theorem DirichletTransform.IsRegCarlsonContinuation.mk_of_eq_realCarlsonDirichletAverage {ι : Type u_1} [Fintype ι] [Nonempty ι] {f : ℂ → ℂ} {z : ι → ℂ} {G H : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G Set.univ) (hH : IsRegCarlsonContinuation f z H) (hEq : ∀ b ∈ ProbabilityTheory.mvRealBetaDomain, (G fun (i : ι) => ↑(b i)) = realCarlsonDirichletAverage b z f / Complex.Gamma (∑ i : ι, ↑(b i))) : IsRegCarlsonContinuation f z G

An entire candidate which has the probability-average values on positive real parameters is a Carlson continuation, provided one continuation is already known to exist. The reference continuation is used only for uniqueness.

theorem DirichletTransform.exists_isRegCarlsonContinuation {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {z : ι → ℂ} (hz : Set.range z ⊆ Ω) : ∃ (G : (ι → ℂ) → ℂ), IsRegCarlsonContinuation f z G

A holomorphic scalar function on a convex open set admits an entire regularized Dirichlet-parameter continuation at every node vector in that set.