Carlson's multivariate T-function

Carlson's Definition 5.12-1 defines T(b,z) as the Dirichlet average of w ↦ exp (1 / w). Carlson immediately turns to a limiting two-variable case; this file keeps the short general multivariate theory separate from that specialization.

The intrinsic variable domain used here says that the convex hull of the variables avoids zero. Carlson's assumption that all variables lie in a common open half-plane not containing zero implies this condition.

References

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

noncomputable def DirichletTransform.carlsonTKernel (w : ℂ) : ℂ

The scalar kernel defining Carlson's T-function.

Equations

• DirichletTransform.carlsonTKernel w = Complex.exp w⁻¹

def DirichletTransform.carlsonTVariableDomain {ι : Type u_1} : Set (ι → ℂ)

The intrinsic multivariate domain on which every convex combination of the variables is nonzero.

Equations

• DirichletTransform.carlsonTVariableDomain = {z : ι → ℂ | 0 ∉ (convexHull ℝ) (Set.range z)}

theorem DirichletTransform.mem_carlsonTVariableDomain_of_range_subset {ι : Type u_1} {H : Set ℂ} (hH : Convex ℝ H) (hzero : 0 ∉ H) {z : ι → ℂ} (hz : Set.range z ⊆ H) : z ∈ carlsonTVariableDomain

Any convex zero-avoiding set containing all variables certifies membership in the intrinsic T-variable domain. Carlson applies this with an open half-plane not containing zero.

theorem DirichletTransform.carlsonAffineForm_ne_zero_of_mem_carlsonTVariableDomain {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonTVariableDomain) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : carlsonAffineForm z u ≠ 0

On the T-variable domain, Carlson's affine form never vanishes on the standard simplex.

theorem DirichletTransform.continuousOn_carlsonTKernel_carlsonAffineForm {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonTVariableDomain) : ContinuousOn (fun (u : ι → ℝ) => carlsonTKernel (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι)

The T-kernel composed with Carlson's affine form is continuous on the simplex whenever the convex hull of the variables avoids zero.

theorem DirichletTransform.analyticOnNhd_carlsonTKernel_carlsonAffineForm {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : AnalyticOnNhd ℂ (fun (z : ι → ℂ) => carlsonTKernel (carlsonAffineForm z u)) carlsonTVariableDomain

For a fixed simplex point, the T-kernel is analytic in all variables throughout the intrinsic zero-avoiding domain.

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

Carlson's native regularized multivariate T-integral.

Equations

• DirichletTransform.regCarlsonTIntegral b z = DirichletTransform.regCarlsonDirichletAverage b z DirichletTransform.carlsonTKernel

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

Carlson's native, unregularized multivariate T-integral from Definition 5.12-1.

Equations

• DirichletTransform.carlsonTIntegral b z = Complex.Gamma (∑ i : ι, b i) * DirichletTransform.regCarlsonTIntegral b z

theorem DirichletTransform.integrableOn_regDirichletDensity_mul_carlsonTKernel {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : z ∈ carlsonTVariableDomain) : MeasureTheory.IntegrableOn (fun (u : ι → ℝ) => ProbabilityTheory.regDirichletDensity b u * carlsonTKernel (carlsonAffineForm z u)) (Convexity.StdSimplex.coordinateSet ℝ ι) MeasureTheory.Measure.stdSimplexMeasure

The native T-integrand is integrable under Carlson's parameter and variable hypotheses.

theorem DirichletTransform.regCarlsonTIntegral_perm {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (σ : Equiv.Perm ι) : regCarlsonTIntegral (b ∘ ⇑σ) (z ∘ ⇑σ) = regCarlsonTIntegral b z

Simultaneous permutation of parameters and variables leaves the native regularized T-integral unchanged.

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

A candidate is an entire regularized continuation of Carlson's T-function in the Dirichlet parameters if it agrees with the native integral on mvBetaConvergent.

Equations

• DirichletTransform.IsRegCarlsonTContinuation z G = DirichletTransform.IsRegCarlsonContinuation DirichletTransform.carlsonTKernel z G

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

A regularized T-continuation is entire in the Dirichlet parameters.

theorem DirichletTransform.IsRegCarlsonTContinuation.eq_integral {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonTContinuation z G) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) : G b = regCarlsonTIntegral b z

A regularized T-continuation agrees with Carlson's native integral on its convergence domain.

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

The entire regularized continuation of T, if it exists, is unique.

theorem DirichletTransform.exists_isRegCarlsonTContinuation {ι : Type u_1} [Fintype ι] {z : ι → ℂ} (hz : z ∈ carlsonTVariableDomain) : ∃ (G : (ι → ℂ) → ℂ), IsRegCarlsonTContinuation z G

The smooth-kernel Dirichlet continuation theorem supplies an entire regularized T-continuation whenever the convex hull of the variables avoids zero. This proof does not construct a contour representation.

theorem DirichletTransform.isOpen_carlsonTVariableDomain {ι : Type u_1} [Finite ι] : IsOpen carlsonTVariableDomain

The intrinsic T-variable domain is open.