Carlson's R-function: continuation in the Dirichlet parameters

For every complex exponent and nodes in the right half-plane, the smooth-kernel Dirichlet continuation theorem supplies a unique entire regularized R-function. regCarlsonRContinued selects this continuation, agrees with the native integral on its convergence region, and recovers the regularized R-polynomials at natural exponents. The node-domain hypothesis is an explicit argument: no continuation in the nodes or across the power's branch cut is claimed.

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

A candidate is an entire regularized continuation of Carlson's R_t if it agrees with the native regularized integral on the ordinary convergence region.

Equations

• DirichletTransform.IsRegCarlsonRContinuation t z G = DirichletTransform.IsRegCarlsonContinuation (fun (w : ℂ) => w ^ t) z G

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

A regularized Carlson R_t continuation is entire in the Dirichlet parameters.

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

A regularized Carlson continuation agrees with the native integral on its convergence domain.

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

An entire regularized continuation of Carlson's R_t, if it exists, is unique.

theorem DirichletTransform.contDiffNearStdSimplex_cpow_carlsonAffineForm {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (N : ℕ) : ContDiffNearStdSimplex N fun (u : ι → ℝ) => carlsonAffineForm z u ^ t

A complex power of the affine form is smooth near the simplex on the right-half-plane node domain. This supplies the hypothesis of the general Dirichlet continuation theorem.

theorem DirichletTransform.exists_isRegCarlsonRContinuation {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : ∃ (G : (ι → ℂ) → ℂ), IsRegCarlsonRContinuation t z G

Every complex exponent has an entire regularized continuation in the Dirichlet parameters, for nodes in the right half-plane. No contour representation is needed.

noncomputable def DirichletTransform.regCarlsonRContinued {ι : Type u_1} [Fintype ι] (t : ℂ) (z : ι → ℂ) (hz : z ∈ carlsonRVariableDomain) : (ι → ℂ) → ℂ

The unique entire regularized R-continuation for right-half-plane nodes. The choice selects a witness of the proved existence theorem; uniqueness makes it canonical.

Equations

• DirichletTransform.regCarlsonRContinued t z hz = ⋯.choose

theorem DirichletTransform.isRegCarlsonRContinuation_continued {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : IsRegCarlsonRContinuation t z (regCarlsonRContinued t z hz)

The selected function is an entire regularized continuation of the native integral.

theorem DirichletTransform.analyticOnNhd_regCarlsonRContinued {ι : Type u_1} [Fintype ι] (t : ℂ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : AnalyticOnNhd ℂ (regCarlsonRContinued t z hz) Set.univ

The continued regularized R-function is entire in all Dirichlet parameters.

theorem DirichletTransform.regCarlsonRContinued_eq_integral {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) (hb : b ∈ Complex.mvBetaConvergent) : regCarlsonRContinued t z hz b = regCarlsonRIntegral t b z

On the convergence region, the continued function is the native regularized integral.

theorem DirichletTransform.IsRegCarlsonRContinuation.eq_continued {ι : Type u_1} [Fintype ι] {t : ℂ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonRContinuation t z G) (hz : z ∈ carlsonRVariableDomain) : G = regCarlsonRContinued t z hz

Any entire continuation agrees with the selected regularized R-function.

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

At a natural exponent, the regularized R-polynomial supplies the entire continuation in the Dirichlet parameters. Thus the general R-function continuation extends, rather than replaces, the polynomial theory of Section 5.7.

theorem DirichletTransform.IsRegCarlsonRContinuation.eq_regCarlsonR_natCast {ι : Type u_1} [Fintype ι] {n : ℕ} {z : ι → ℂ} {G : (ι → ℂ) → ℂ} (hG : IsRegCarlsonRContinuation (↑n) z G) : G = regCarlsonR n z

Any entire regularized continuation at a natural exponent equals the corresponding regularized R-polynomial.

theorem DirichletTransform.regCarlsonRContinued_natCast {ι : Type u_1} [Fintype ι] (n : ℕ) {z : ι → ℂ} (hz : z ∈ carlsonRVariableDomain) : regCarlsonRContinued (↑n) z hz = regCarlsonR n z

At natural exponents the selected continuation recovers the existing R-polynomial.